![]() |
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 412 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | 2 | imdistani 568 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒)) |
4 | syldanl.2 | . 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏) | |
5 | 3, 4 | sylan 579 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 |
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 396 |
This theorem is referenced by: sylanl2 678 oen0 8582 oeordsuc 8590 erth 8749 phplem2 9205 lo1bdd2 15466 grplmulf1o 18934 grplactcnv 18963 trust 24058 efrlim 26820 efrlimOLD 26821 fedgmullem2 33197 submateq 33281 heibor1lem 37171 idlnegcl 37384 igenmin 37426 eqvrelth 37975 sticksstones22 41481 binomcxplemnotnn0 43629 vonioolem1 45906 vonicclem1 45909 smfsuplem1 46037 smflimsuplem4 46049 |
Copyright terms: Public domain | W3C validator |