![]() |
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 132 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mtbi 671 |
1
![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: nnexmid 851 nndc 852 fal 1371 ax-9 1542 nonconne 2372 nemtbir 2449 ru 2976 noel 3441 iun0 3958 0iun 3959 br0 4066 vprc 4150 iin0r 4187 nlim0 4412 snnex 4466 onsucelsucexmid 4547 0nelxp 4672 dm0 4859 iprc 4913 co02 5160 0fv 5570 frec0g 6422 nnsucuniel 6520 1nen2 6889 fidcenumlemrk 6983 djulclb 7084 ismkvnex 7183 pw1ne3 7259 sucpw1nel3 7262 3nsssucpw1 7265 0nnq 7393 0npr 7512 nqprdisj 7573 0ncn 7860 axpre-ltirr 7911 pnfnre 8029 mnfnre 8030 inelr 8571 xrltnr 9809 fzo0 10198 fzouzdisj 10210 inftonninf 10472 hashinfom 10790 3prm 12160 sqrt2irr 12194 ennnfonelem1 12458 bj-nndcALT 14971 bj-vprc 15109 pwle2 15210 exmidsbthrlem 15232 |
Copyright terms: Public domain | W3C validator |