Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > syld3an2 | Structured version Visualization 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 1271 | . . 3 |
3 | syld3an2.2 | . . . 4 | |
4 | 3 | 3com23 1271 | . . 3 |
5 | 2, 4 | syld3an3 1371 | . 2 |
6 | 5 | 3com23 1271 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 w3a 1037 |
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 197 df-an 386 df-3an 1039 |
This theorem is referenced by: nppcan2 10312 nnncan 10316 nnncan2 10318 ltdivmul 10898 ledivmul 10899 ltdiv23 10914 lediv23 10915 xrmaxlt 12012 xrltmin 12013 xrmaxle 12014 xrlemin 12015 swrdtrcfv 13441 dvdssub2 15023 dvdsgcdb 15262 lcmdvdsb 15326 vdwapun 15678 poslubdg 17149 ipodrsfi 17163 mulginvcom 17565 matinvgcell 20241 mdetrsca2 20410 mdetrlin2 20413 mdetunilem5 20422 decpmatmul 20577 islp3 20950 bddibl 23606 nvpi 27522 nvabs 27527 nmmulg 30012 subdivcomb2 31612 lineid 32190 oplecon1b 34488 opltcon1b 34492 oldmm2 34505 oldmj2 34509 cmt3N 34538 2llnneN 34695 cvrexchlem 34705 pmod2iN 35135 polcon2N 35205 paddatclN 35235 osumcllem3N 35244 ltrnval1 35420 cdleme48fv 35787 cdlemg33b 35995 trlcolem 36014 cdlemh 36105 cdlemi1 36106 cdlemi2 36107 cdlemi 36108 cdlemk4 36122 cdlemk19u1 36257 cdlemn3 36486 hgmapfval 37178 pell14qrgap 37439 stoweidlem22 40239 stoweidlem26 40243 sigarexp 41048 pfxtrcfv 41401 pfxco 41438 lindszr 42258 |
Copyright terms: Public domain | W3C validator |