Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mtbiri | Unicode version |
Description: An inference from a biconditional, similar to modus tollens. (Contributed by NM, 24-Aug-1995.) |
Ref | Expression |
---|---|
mtbiri.min | |
mtbiri.maj |
Ref | Expression |
---|---|
mtbiri |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mtbiri.min | . 2 | |
2 | mtbiri.maj | . . 3 | |
3 | 2 | biimpd 143 | . 2 |
4 | 1, 3 | mtoi 654 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-in1 604 ax-in2 605 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: n0i 3399 axnul 4089 intexr 4111 intnexr 4112 iin0r 4130 exmid01 4159 ordtriexmidlem 4477 ordtriexmidlem2 4478 ordtri2or2exmidlem 4484 onsucelsucexmidlem 4487 sucprcreg 4507 preleq 4513 reg3exmidlemwe 4537 dcextest 4539 nn0eln0 4578 0nelelxp 4614 canth 5775 tfrlemisucaccv 6269 nnsucuniel 6439 nndceq 6443 nndcel 6444 2dom 6747 snnen2oprc 6802 snexxph 6891 elfi2 6913 djune 7017 updjudhcoinrg 7020 omp1eomlem 7033 nnnninfeq 7066 ismkvnex 7093 mkvprop 7096 omniwomnimkv 7105 exmidfodomrlemrALT 7133 exmidaclem 7138 elni2 7229 ltsopi 7235 ltsonq 7313 renepnf 7920 renemnf 7921 lt0ne0d 8383 sup3exmid 8823 nnne0 8856 nn0ge2m1nn 9145 nn0nepnf 9156 xrltnr 9681 pnfnlt 9689 nltmnf 9690 xrltnsym 9695 xrlttri3 9699 nltpnft 9713 ngtmnft 9716 xrrebnd 9718 xrpnfdc 9741 xrmnfdc 9742 xsubge0 9780 xposdif 9781 xleaddadd 9786 fzpreddisj 9968 fzm1 9997 exfzdc 10134 xrbdtri 11168 m1exp1 11786 3prm 11999 prmdc 12001 exmidunben 12142 unct 12158 blssioo 12932 pilem3 13091 bj-charfunbi 13373 bj-intexr 13470 bj-intnexr 13471 subctctexmid 13560 nninfsellemeq 13573 exmidsbthrlem 13580 |
Copyright terms: Public domain | W3C validator |