| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > syland | Structured version Visualization version GIF version | ||
| Description: A syllogism deduction. (Contributed by NM, 15-Dec-2004.) |
| Ref | Expression |
|---|---|
| syland.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
| syland.2 | ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜏)) |
| Ref | Expression |
|---|---|
| syland | ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜏)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | syland.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
| 2 | syland.2 | . . . 4 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜏)) | |
| 3 | 2 | expd 415 | . . 3 ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) |
| 4 | 1, 3 | syld 47 | . 2 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏))) |
| 5 | 4 | impd 410 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜏)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 |
| This theorem is referenced by: sylani 604 sylan2d 605 syl2and 608 onfununi 8381 fodomfir 9368 lt2add 11748 nn0seqcvgd 16607 1stcelcls 23469 llyidm 23496 filuni 23893 ballotlemimin 34508 btwnintr 36020 ifscgr 36045 btwnconn1lem12 36099 poimir 37660 cvrntr 39427 goldbachthlem2 47533 |
| Copyright terms: Public domain | W3C validator |