Metamath Proof Explorer


Theorem syldbl2

Description: Stacked hypotheseis implies goal. (Contributed by Stanislas Polu, 9-Mar-2020)

Ref Expression
Hypothesis syldbl2.1 ⊢ φ ∧ ψ → ψ → θ
Assertion syldbl2 ⊢ φ ∧ ψ → θ

Proof

Step Hyp Ref Expression
1 syldbl2.1 ⊢ φ ∧ ψ → ψ → θ
2 1 com12 ⊢ ψ → φ ∧ ψ → θ
3 2 anabsi7 ⊢ φ ∧ ψ → θ