![]() |
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 | syld3an2.1 | . . . 4 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜓) | |
2 | 1 | 3com23 1263 | . . 3 ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜒) → 𝜓) |
3 | syld3an2.2 | . . . 4 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) | |
4 | 3 | 3com23 1263 | . . 3 ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜏) |
5 | 2, 4 | syld3an3 1363 | . 2 ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜒) → 𝜏) |
6 | 5 | 3com23 1263 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: nppcan2 10191 nnncan 10195 nnncan2 10197 ltdivmul 10777 ledivmul 10778 ltdiv23 10793 lediv23 10794 xrmaxlt 11886 xrltmin 11887 xrmaxle 11888 xrlemin 11889 swrdtrcfv 13293 dvdssub2 14861 dvdsgcdb 15100 lcmdvdsb 15164 vdwapun 15516 poslubdg 16972 ipodrsfi 16986 mulginvcom 17388 matinvgcell 20060 mdetrsca2 20229 mdetrlin2 20232 mdetunilem5 20241 decpmatmul 20396 islp3 20760 bddibl 23412 nvpi 26906 nvabs 26911 nmmulg 29340 subdivcomb2 30865 lineid 31360 oplecon1b 33506 opltcon1b 33510 oldmm2 33523 oldmj2 33527 cmt3N 33556 2llnneN 33713 cvrexchlem 33723 pmod2iN 34153 polcon2N 34223 paddatclN 34253 osumcllem3N 34262 ltrnval1 34438 cdleme48fv 34805 cdlemg33b 35013 trlcolem 35032 cdlemh 35123 cdlemi1 35124 cdlemi2 35125 cdlemi 35126 cdlemk4 35140 cdlemk19u1 35275 cdlemn3 35504 hgmapfval 36196 pell14qrgap 36457 stoweidlem22 38915 stoweidlem26 38919 sigarexp 39697 pfxtrcfv 40264 pfxco 40301 lindszr 42052 |
Copyright terms: Public domain | W3C validator |