![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mtbir | Unicode version |
Description: An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 14-Oct-2012.) |
Ref | Expression |
---|---|
mtbir.1 |
![]() ![]() ![]() |
mtbir.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mtbir |
![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mtbir.1 |
. 2
![]() ![]() ![]() | |
2 | mtbir.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | bicomi 123 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mtbi 594 |
1
![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in1 544 ax-in2 545 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: fal 1249 ax-9 1421 nonconne 2212 nemtbir 2288 ru 2757 pssirr 3038 noel 3222 npss0 3260 iun0 3704 0iun 3705 vprc 3879 iin0r 3913 nlim0 4097 snnex 4147 onsucelsucexmid 4215 0nelxp 4315 dm0 4492 iprc 4543 co02 4777 0fv 5151 frec0g 5922 0nnq 6348 0npr 6466 nqprdisj 6527 0ncn 6729 axpre-ltirr 6766 pnfnre 6864 mnfnre 6865 inelr 7368 xrltnr 8471 fzo0 8794 fzouzdisj 8806 nnexmid 9234 nndc 9235 bj-vprc 9351 |
Copyright terms: Public domain | W3C validator |