![]() |
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 1133 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜑) | |
2 | syld3an2.1 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜓) | |
3 | simp3 1135 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜃) | |
4 | syld3an2.2 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) | |
5 | 1, 2, 3, 4 | syl3anc 1368 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1084 |
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 395 df-3an 1086 |
This theorem is referenced by: enfii 9220 domsdomtrfi 9236 nppcan2 11529 nnncan 11533 nnncan2 11535 subdivcomb2 11948 ltdivmul 12127 ledivmul 12128 ltdiv23 12143 lediv23 12144 xrmaxlt 13200 xrltmin 13201 xrmaxle 13202 xrlemin 13203 pfxtrcfv 14683 pfxco 14829 dvdssub2 16285 dvdsgcdb 16528 lcmdvdsb 16591 vdwapun 16950 poslubdg 18413 ipodrsfi 18538 mulginvcom 19061 matinvgcell 22357 mdetrsca2 22526 mdetrlin2 22529 mdetunilem5 22538 decpmatmul 22694 islp3 23070 bddibl 25789 nvpi 30497 nvabs 30502 nmmulg 33602 lineid 35712 oplecon1b 38705 opltcon1b 38709 oldmm2 38722 oldmj2 38726 cmt3N 38755 2llnneN 38914 cvrexchlem 38924 pmod2iN 39354 polcon2N 39424 paddatclN 39454 osumcllem3N 39463 ltrnval1 39639 cdleme48fv 40004 cdlemg33b 40212 trlcolem 40231 cdlemh 40322 cdlemi1 40323 cdlemi2 40324 cdlemi 40325 cdlemk4 40339 cdlemk19u1 40474 cdlemn3 40702 hgmapfval 41391 pell14qrgap 42326 mnringmulrcld 43696 stoweidlem22 45439 stoweidlem26 45443 sigarexp 46276 lindszr 47615 fv2arycl 47799 |
Copyright terms: Public domain | W3C validator |