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 418 | . . 3 ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) |
4 | 1, 3 | syld 47 | . 2 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏))) |
5 | 4 | impd 413 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 |
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 209 df-an 399 |
This theorem is referenced by: sylani 605 sylan2d 606 syl2and 609 onfununi 7981 lt2add 11128 nn0seqcvgd 15917 1stcelcls 22072 llyidm 22099 filuni 22496 ballotlemimin 31767 btwnintr 33484 ifscgr 33509 btwnconn1lem12 33563 poimir 34929 cvrntr 36565 goldbachthlem2 43715 |
Copyright terms: Public domain | W3C validator |