![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > syld3an2 | Structured version Unicode version |
Description: A syllogism inference. (Contributed by NM, 20-May-2007.) |
Ref | Expression |
---|---|
syld3an2.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
syld3an2.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syld3an2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syld3an2.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 3com23 1194 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | syld3an2.2 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | 3com23 1194 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | syld3an3 1264 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | 3com23 1194 |
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 185 df-an 371 df-3an 967 |
This theorem is referenced by: nppcan2 9746 nnncan 9750 nnncan2 9752 ltdivmul 10310 ledivmul 10311 ltdiv23 10329 lediv23 10330 xrmaxlt 11259 xrltmin 11260 xrmaxle 11261 xrlemin 11262 swrdtrcfv 12450 dvdssub2 13683 dvdsgcdb 13841 vdwapun 14148 poslubdg 15433 ipodrsfi 15447 mdetrsca2 18537 mdetrlin2 18540 mdetunilem5 18549 islp3 18877 bddibl 21445 gxinv 23904 gxinv2 23905 vcnegsubdi2 24100 nvpi 24201 nvabs 24208 nmmulg 26537 ghomgsg 27451 subdivcomb2 27524 lineid 28253 pell14qrgap 29359 stoweidlem22 29960 stoweidlem26 29964 sigarexp 30038 matinvgcell 31014 lindszr 31117 decpmatmul 31241 oplecon1b 33165 opltcon1b 33169 oldmm2 33182 oldmj2 33186 cmt3N 33215 2llnneN 33372 cvrexchlem 33382 pmod2iN 33812 polcon2N 33882 paddatclN 33912 osumcllem3N 33921 ltrnval1 34097 cdleme48fv 34462 cdlemg33b 34670 trlcolem 34689 cdlemh 34780 cdlemi1 34781 cdlemi2 34782 cdlemi 34783 cdlemk4 34797 cdlemk19u1 34932 cdlemn3 35161 hgmapfval 35853 |
Copyright terms: Public domain | W3C validator |