Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > syldanl | Structured version Visualization version GIF version |
Description: A syllogism deduction with conjoined antecedents. (Contributed by Jeff Madsen, 20-Jun-2011.) |
Ref | Expression |
---|---|
syldanl.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
syldanl.2 | ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
syldanl | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syldanl.1 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
2 | 1 | ex 415 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | 2 | imdistani 571 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒)) |
4 | syldanl.2 | . 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏) | |
5 | 3, 4 | sylan 582 | 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: sylanl2 679 oen0 8211 oeordsuc 8219 erth 8337 lo1bdd2 14880 grplmulf1o 18172 grplactcnv 18201 trust 22837 efrlim 25546 fedgmullem2 31026 submateq 31074 heibor1lem 35086 idlnegcl 35299 igenmin 35341 eqvrelth 35845 binomcxplemnotnn0 40686 vonioolem1 42961 vonicclem1 42964 smfsuplem1 43084 smflimsuplem4 43096 |
Copyright terms: Public domain | W3C validator |