Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl2anr | Unicode version |
Description: A double syllogism inference. (Contributed by NM, 17-Sep-2013.) |
Ref | Expression |
---|---|
syl2an.1 | |
syl2an.2 | |
syl2an.3 |
Ref | Expression |
---|---|
syl2anr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl2an.1 | . . 3 | |
2 | syl2an.2 | . . 3 | |
3 | syl2an.3 | . . 3 | |
4 | 1, 2, 3 | syl2an 287 | . 2 |
5 | 4 | ancoms 266 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: swopo 4223 opswapg 5020 coexg 5078 iotass 5100 resdif 5382 fvexg 5433 isotr 5710 xpexgALT 6024 ixpssmapg 6615 mapen 6733 mapdom1g 6734 elfir 6854 cauappcvgprlemladdfl 7456 addgt0sr 7576 axmulass 7674 axdistr 7675 negeu 7946 ltaddnegr 8180 nnsub 8752 zltnle 9093 elz2 9115 uzaddcl 9374 qaddcl 9420 xltneg 9612 xleneg 9613 iccneg 9765 uzsubsubfz 9820 fzsplit2 9823 fzss1 9836 uzsplit 9865 fz0fzdiffz0 9900 difelfzle 9904 difelfznle 9905 fzonlt0 9937 fzouzsplit 9949 eluzgtdifelfzo 9967 elfzodifsumelfzo 9971 ssfzo12 9994 qltnle 10016 modfzo0difsn 10161 nn0ennn 10199 ser3mono 10244 iseqf1olemjpcl 10261 iseqf1olemqpcl 10262 fser0const 10282 faclbnd 10480 bcval4 10491 bcpasc 10505 hashfacen 10572 seq3coll 10578 crim 10623 fsumshftm 11207 isumshft 11252 cvgratgt0 11295 mertenslemi1 11297 negdvdsb 11498 dvdsnegb 11499 dvdsmul1 11504 dvdsabseq 11534 dvdsssfz1 11539 odd2np1 11559 ndvdsadd 11617 dvdssqim 11701 nn0seqcvgd 11711 algcvgblem 11719 cncongr2 11774 prmind2 11790 prmdvdsfz 11808 prmndvdsfaclt 11823 resttopon 12329 cnovex 12354 iscn 12355 iscnp 12357 cnco 12379 cndis 12399 hmeoco 12474 bl2in 12561 metss2lem 12655 metss2 12656 bdxmet 12659 metrest 12664 ioo2bl 12701 elcncf 12718 dvexp 12833 supfz 13226 |
Copyright terms: Public domain | W3C validator |