![]() |
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: ![]() ![]() |
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 4236 opswapg 5033 coexg 5091 iotass 5113 resdif 5397 fvexg 5448 isotr 5725 xpexgALT 6039 ixpssmapg 6630 mapen 6748 mapdom1g 6749 elfir 6869 cauappcvgprlemladdfl 7487 addgt0sr 7607 axmulass 7705 axdistr 7706 negeu 7977 ltaddnegr 8211 nnsub 8783 zltnle 9124 elz2 9146 uzaddcl 9408 qaddcl 9454 xltneg 9649 xleneg 9650 iccneg 9802 uzsubsubfz 9858 fzsplit2 9861 fzss1 9874 uzsplit 9903 fz0fzdiffz0 9938 difelfzle 9942 difelfznle 9943 fzonlt0 9975 fzouzsplit 9987 eluzgtdifelfzo 10005 elfzodifsumelfzo 10009 ssfzo12 10032 qltnle 10054 modfzo0difsn 10199 nn0ennn 10237 ser3mono 10282 iseqf1olemjpcl 10299 iseqf1olemqpcl 10300 fser0const 10320 faclbnd 10519 bcval4 10530 bcpasc 10544 hashfacen 10611 seq3coll 10617 crim 10662 fsumshftm 11246 isumshft 11291 cvgratgt0 11334 mertenslemi1 11336 negdvdsb 11545 dvdsnegb 11546 dvdsmul1 11551 dvdsabseq 11581 dvdsssfz1 11586 odd2np1 11606 ndvdsadd 11664 dvdssqim 11748 nn0seqcvgd 11758 algcvgblem 11766 cncongr2 11821 prmind2 11837 prmdvdsfz 11855 prmndvdsfaclt 11870 resttopon 12379 cnovex 12404 iscn 12405 iscnp 12407 cnco 12429 cndis 12449 hmeoco 12524 bl2in 12611 metss2lem 12705 metss2 12706 bdxmet 12709 metrest 12714 ioo2bl 12751 elcncf 12768 dvexp 12883 relogexp 13001 logcxp 13026 supfz 13428 |
Copyright terms: Public domain | W3C validator |