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 416 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | 2 | imdistani 572 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒)) |
4 | syldanl.2 | . 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏) | |
5 | 3, 4 | sylan 583 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: sylanl2 681 oen0 8236 oeordsuc 8244 erth 8362 lo1bdd2 14964 grplmulf1o 18284 grplactcnv 18313 trust 22974 efrlim 25699 fedgmullem2 31275 submateq 31323 heibor1lem 35579 idlnegcl 35792 igenmin 35834 eqvrelth 36336 binomcxplemnotnn0 41496 vonioolem1 43744 vonicclem1 43747 smfsuplem1 43867 smflimsuplem4 43879 |
Copyright terms: Public domain | W3C validator |