![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sylanb | Structured version Visualization version Unicode version |
Description: A syllogism inference. (Contributed by NM, 18-May-1994.) |
Ref | Expression |
---|---|
sylanb.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
sylanb.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
sylanb |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylanb.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biimpi 199 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
3 | sylanb.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | sylan 478 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 190 df-an 377 |
This theorem is referenced by: syl2anb 486 anabsan 827 eqtr2 2482 pm13.181 2718 rmob 3371 sspsstr 3550 disjne 3822 seex 4819 xpcan2 5296 tron 5469 fssres 5776 funbrfvb 5934 funopfvb 5935 fvco 5969 fvimacnvi 6024 ffvresb 6083 funressn 6106 funresdfunsn 6135 fvtp2 6141 fvtp2g 6144 fnex 6162 funex 6163 ordsucss 6677 ordsucelsuc 6681 1st2nd 6871 frxp 6938 dftpos4 7023 tz7.48lem 7189 nnmsucr 7357 nnmcan 7366 xpmapenlem 7770 php 7787 php4 7790 isfinite2 7860 fundmfibi 7886 fiinfcl 8048 wofib 8091 r1limg 8273 r1pwcl 8349 cardmin2 8463 zornn0g 8966 intgru 9270 supsrlem 9566 fnn0ind 11068 uztrn2 11210 nnwo 11258 irradd 11322 qbtwnxr 11527 xltnegi 11543 xaddnemnf 11561 xaddnepnf 11562 xaddcom 11565 xnegdi 11568 elioore 11700 uzsubsubfz1 11857 fzo1fzo0n0 11994 elfzonelfzo 12048 leexp2 12365 faclbnd 12513 faclbnd3 12515 fi1uzind 12689 brfi1uzind 12690 opfi1uzind 12693 swrdccat3b 12895 dvdslelem 14404 divalglem1 14427 isprm2lem 14686 dvdsprime 14692 pcgcd 14882 cntri 17039 efgsrel 17439 xrsdsreclb 19070 znf1o 19177 restuni 20233 stoig 20234 restperf 20255 resstps 20258 pnfnei 20291 mnfnei 20292 cnnei 20353 cmpsublem 20469 comppfsc 20602 tx1stc 20720 xkopt 20725 isfcls 21079 tgioo 21869 opnreen 21904 iscmet3 22318 dyaddisj 22610 limcmpt 22894 degltlem1 23077 ulmdvlem3 23413 lgsdi 24316 clwlkfclwwlk 25628 2wlkonotv 25661 eupath2lem3 25763 grpoidinvlem3 25990 ipasslem3 26530 spanuni 27253 5oalem3 27365 5oalem5 27367 mdslmd1lem2 28035 mptct 28354 mptctf 28357 xaddeq0 28382 ordtconlem1 28781 esumcvg 28958 ldgenpisyslem1 29036 measres 29095 measdivcstOLD 29097 measdivcst 29098 probun 29302 elmpps 30261 dfon2lem9 30487 noreson 30597 funpartfun 30760 cgrxfr 30872 segcon2 30922 brsegle2 30926 seglecgr12im 30927 segletr 30931 nn0prpw 31029 bj-seex 31572 ptrecube 31986 poimirlem28 32014 ftc1anclem5 32067 ftc1anc 32071 exlimddvfi 32408 prtlem11 32484 mzpclall 35615 4an31 36899 iundjiun 38403 funbrafvb 38793 funopafvb 38794 afvco2 38813 cusgrres 39655 usgfis 40127 usgfisALT 40131 |
Copyright terms: Public domain | W3C validator |