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 1137 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜑) | |
2 | syld3an2.1 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜓) | |
3 | simp3 1139 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜃) | |
4 | syld3an2.2 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) | |
5 | 1, 2, 3, 4 | syl3anc 1372 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1088 |
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 210 df-an 400 df-3an 1090 |
This theorem is referenced by: enfii 8784 nppcan2 10995 nnncan 10999 nnncan2 11001 subdivcomb2 11414 ltdivmul 11593 ledivmul 11594 ltdiv23 11609 lediv23 11610 xrmaxlt 12657 xrltmin 12658 xrmaxle 12659 xrlemin 12660 pfxtrcfv 14144 pfxco 14289 dvdssub2 15746 dvdsgcdb 15989 lcmdvdsb 16054 vdwapun 16410 poslubdg 17875 ipodrsfi 17889 mulginvcom 18370 matinvgcell 21186 mdetrsca2 21355 mdetrlin2 21358 mdetunilem5 21367 decpmatmul 21523 islp3 21897 bddibl 24592 nvpi 28602 nvabs 28607 nmmulg 31488 lineid 34023 oplecon1b 36838 opltcon1b 36842 oldmm2 36855 oldmj2 36859 cmt3N 36888 2llnneN 37046 cvrexchlem 37056 pmod2iN 37486 polcon2N 37556 paddatclN 37586 osumcllem3N 37595 ltrnval1 37771 cdleme48fv 38136 cdlemg33b 38344 trlcolem 38363 cdlemh 38454 cdlemi1 38455 cdlemi2 38456 cdlemi 38457 cdlemk4 38471 cdlemk19u1 38606 cdlemn3 38834 hgmapfval 39523 pell14qrgap 40269 mnringmulrcld 41388 stoweidlem22 43105 stoweidlem26 43109 sigarexp 43914 lindszr 45344 fv2arycl 45528 |
Copyright terms: Public domain | W3C validator |