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 659 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 603 ax-in2 604 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: nnexmid 835 nndc 836 fal 1338 ax-9 1511 nonconne 2318 nemtbir 2395 ru 2903 noel 3362 iun0 3864 0iun 3865 br0 3971 vprc 4055 iin0r 4088 nlim0 4311 snnex 4364 onsucelsucexmid 4440 0nelxp 4562 dm0 4748 iprc 4802 co02 5047 0fv 5449 frec0g 6287 nnsucuniel 6384 1nen2 6748 fidcenumlemrk 6835 djulclb 6933 ismkvnex 7022 0nnq 7165 0npr 7284 nqprdisj 7345 0ncn 7632 axpre-ltirr 7683 pnfnre 7800 mnfnre 7801 inelr 8339 xrltnr 9559 fzo0 9938 fzouzdisj 9950 inftonninf 10207 hashinfom 10517 3prm 11798 sqrt2irr 11829 ennnfonelem1 11909 bj-nndcALT 12952 bj-vprc 13083 pwle2 13182 exmidsbthrlem 13206 |
Copyright terms: Public domain | W3C validator |