![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syld3an2 | Structured version Visualization version GIF 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 | simp1 1170 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜑) | |
2 | syld3an2.1 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜓) | |
3 | simp3 1172 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜃) | |
4 | syld3an2.2 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) | |
5 | 1, 2, 3, 4 | syl3anc 1494 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1111 |
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 199 df-an 387 df-3an 1113 |
This theorem is referenced by: nppcan2 10640 nnncan 10644 nnncan2 10646 subdivcomb2 11054 ltdivmul 11235 ledivmul 11236 ltdiv23 11251 lediv23 11252 xrmaxlt 12307 xrltmin 12308 xrmaxle 12309 xrlemin 12310 swrdtrcfvOLD 13737 pfxtrcfv 13779 pfxco 13966 dvdssub2 15407 dvdsgcdb 15642 lcmdvdsb 15706 vdwapun 16056 poslubdg 17509 ipodrsfi 17523 mulginvcom 17925 matinvgcell 20615 mdetrsca2 20785 mdetrlin2 20788 mdetunilem5 20797 decpmatmul 20954 islp3 21328 bddibl 24012 nvpi 28073 nvabs 28078 nmmulg 30553 lineid 32724 oplecon1b 35271 opltcon1b 35275 oldmm2 35288 oldmj2 35292 cmt3N 35321 2llnneN 35479 cvrexchlem 35489 pmod2iN 35919 polcon2N 35989 paddatclN 36019 osumcllem3N 36028 ltrnval1 36204 cdleme48fv 36569 cdlemg33b 36777 trlcolem 36796 cdlemh 36887 cdlemi1 36888 cdlemi2 36889 cdlemi 36890 cdlemk4 36904 cdlemk19u1 37039 cdlemn3 37267 hgmapfval 37956 pell14qrgap 38278 stoweidlem22 41027 stoweidlem26 41031 sigarexp 41836 lindszr 43119 |
Copyright terms: Public domain | W3C validator |