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 1135 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜑) | |
2 | syld3an2.1 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜓) | |
3 | simp3 1137 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜃) | |
4 | syld3an2.2 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) | |
5 | 1, 2, 3, 4 | syl3anc 1370 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1086 |
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 206 df-an 397 df-3an 1088 |
This theorem is referenced by: enfii 8981 domsdomtrfi 8997 nppcan2 11261 nnncan 11265 nnncan2 11267 subdivcomb2 11680 ltdivmul 11859 ledivmul 11860 ltdiv23 11875 lediv23 11876 xrmaxlt 12924 xrltmin 12925 xrmaxle 12926 xrlemin 12927 pfxtrcfv 14415 pfxco 14560 dvdssub2 16019 dvdsgcdb 16262 lcmdvdsb 16327 vdwapun 16684 poslubdg 18141 ipodrsfi 18266 mulginvcom 18737 matinvgcell 21593 mdetrsca2 21762 mdetrlin2 21765 mdetunilem5 21774 decpmatmul 21930 islp3 22306 bddibl 25013 nvpi 29038 nvabs 29043 nmmulg 31927 lineid 34394 oplecon1b 37222 opltcon1b 37226 oldmm2 37239 oldmj2 37243 cmt3N 37272 2llnneN 37430 cvrexchlem 37440 pmod2iN 37870 polcon2N 37940 paddatclN 37970 osumcllem3N 37979 ltrnval1 38155 cdleme48fv 38520 cdlemg33b 38728 trlcolem 38747 cdlemh 38838 cdlemi1 38839 cdlemi2 38840 cdlemi 38841 cdlemk4 38855 cdlemk19u1 38990 cdlemn3 39218 hgmapfval 39907 pell14qrgap 40704 mnringmulrcld 41853 stoweidlem22 43570 stoweidlem26 43574 sigarexp 44386 lindszr 45821 fv2arycl 46005 |
Copyright terms: Public domain | W3C validator |