![]() |
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 416 | . . 3 ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) |
4 | 1, 3 | syld 47 | . 2 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏))) |
5 | 4 | impd 411 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: sylani 603 sylan2d 604 syl2and 607 onfununi 7837 lt2add 10979 nn0seqcvgd 15747 1stcelcls 21757 llyidm 21784 filuni 22181 ballotlemimin 31376 btwnintr 33091 ifscgr 33116 btwnconn1lem12 33170 poimir 34477 cvrntr 36113 goldbachthlem2 43212 |
Copyright terms: Public domain | W3C validator |