| 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 1373 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ w3a 1087 |
| 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: enfii 9226 domsdomtrfi 9242 nppcan2 11540 nnncan 11544 nnncan2 11546 div11 11950 subdivcomb2 11963 ltdivmul 12143 ledivmul 12144 ltdiv23 12159 lediv23 12160 xrmaxlt 13223 xrltmin 13224 xrmaxle 13225 xrlemin 13226 pfxtrcfv 14731 pfxco 14877 dvdssub2 16338 dvdsgcdb 16582 lcmdvdsb 16650 vdwapun 17012 poslubdg 18459 ipodrsfi 18584 mulginvcom 19117 matinvgcell 22441 mdetrsca2 22610 mdetrlin2 22613 mdetunilem5 22622 decpmatmul 22778 islp3 23154 bddibl 25875 nvpi 30686 nvabs 30691 nmmulg 33967 lineid 36084 oplecon1b 39202 opltcon1b 39206 oldmm2 39219 oldmj2 39223 cmt3N 39252 2llnneN 39411 cvrexchlem 39421 pmod2iN 39851 polcon2N 39921 paddatclN 39951 osumcllem3N 39960 ltrnval1 40136 cdleme48fv 40501 cdlemg33b 40709 trlcolem 40728 cdlemh 40819 cdlemi1 40820 cdlemi2 40821 cdlemi 40822 cdlemk4 40836 cdlemk19u1 40971 cdlemn3 41199 hgmapfval 41888 pell14qrgap 42886 mnringmulrcld 44247 stoweidlem22 46037 stoweidlem26 46041 sigarexp 46874 lindszr 48386 fv2arycl 48569 |
| Copyright terms: Public domain | W3C validator |