![]() |
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 400 | . . 3 ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) |
4 | 1, 3 | syld 47 | . 2 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏))) |
5 | 4 | impd 396 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 |
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 197 df-an 383 |
This theorem is referenced by: sylani 591 sylan2d 592 syl2and 595 onfununi 7589 lt2add 10713 nn0seqcvgd 15484 1stcelcls 21478 llyidm 21505 filuni 21902 ballotlemimin 30900 btwnintr 32456 ifscgr 32481 btwnconn1lem12 32535 poimir 33768 cvrntr 35226 goldbachthlem2 41979 |
Copyright terms: Public domain | W3C validator |