![]() |
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 413 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | 2 | imdistani 569 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒)) |
4 | syldanl.2 | . 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏) | |
5 | 3, 4 | sylan 580 | 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 206 df-an 397 |
This theorem is referenced by: sylanl2 679 oen0 8585 oeordsuc 8593 erth 8751 phplem2 9207 lo1bdd2 15467 grplmulf1o 18896 grplactcnv 18925 trust 23733 efrlim 26471 fedgmullem2 32710 submateq 32784 heibor1lem 36672 idlnegcl 36885 igenmin 36927 eqvrelth 37476 sticksstones22 40979 binomcxplemnotnn0 43105 vonioolem1 45386 vonicclem1 45389 smfsuplem1 45517 smflimsuplem4 45529 |
Copyright terms: Public domain | W3C validator |