![]() |
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 131 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mtbi 631 |
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 105 ax-ia2 106 ax-ia3 107 ax-in1 580 ax-in2 581 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: fal 1297 ax-9 1470 nonconne 2268 nemtbir 2345 ru 2840 noel 3291 iun0 3792 0iun 3793 vprc 3977 iin0r 4010 nlim0 4230 snnex 4283 onsucelsucexmid 4359 0nelxp 4479 dm0 4663 iprc 4714 co02 4957 0fv 5352 frec0g 6176 nnsucuniel 6270 1nen2 6631 fidcenumlemrk 6717 djulclb 6801 0nnq 6984 0npr 7103 nqprdisj 7164 0ncn 7430 axpre-ltirr 7478 pnfnre 7590 mnfnre 7591 inelr 8122 xrltnr 9311 fzo0 9640 fzouzdisj 9652 inftonninf 9908 hashinfom 10247 3prm 11449 sqrt2irr 11480 nnexmid 11933 nndc 11934 bj-vprc 12060 exmidsbthrlem 12184 |
Copyright terms: Public domain | W3C validator |