![]() |
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 403 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | 2 | imdistani 564 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒)) |
4 | syldanl.2 | . 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏) | |
5 | 3, 4 | sylan 575 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 |
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 199 df-an 387 |
This theorem is referenced by: oen0 7950 oeordsuc 7958 erth 8073 lo1bdd2 14663 grplmulf1o 17876 grplactcnv 17905 trust 22441 submateq 30473 heibor1lem 34232 idlnegcl 34445 igenmin 34487 eqvrelth 34981 binomcxplemnotnn0 39511 vonioolem1 41821 vonicclem1 41824 smfsuplem1 41944 smflimsuplem4 41956 |
Copyright terms: Public domain | W3C validator |