![]() |
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 417 | . . 3 ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) |
4 | 1, 3 | syld 47 | . 2 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏))) |
5 | 4 | impd 412 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 206 df-an 398 |
This theorem is referenced by: sylani 605 sylan2d 606 syl2and 609 onfununi 8341 lt2add 11699 nn0seqcvgd 16507 1stcelcls 22965 llyidm 22992 filuni 23389 ballotlemimin 33535 btwnintr 35022 ifscgr 35047 btwnconn1lem12 35101 poimir 36569 cvrntr 38344 goldbachthlem2 46262 |
Copyright terms: Public domain | W3C validator |