Metamath Proof Explorer


Theorem a1i13

Description: Add two antecedents to a wff. (Contributed by Jeff Hankins, 4-Aug-2009)

Ref Expression
Hypothesis a1i13.1 ⊢ ψ → θ
Assertion a1i13 ⊢ φ → ψ → χ → θ

Proof

Step Hyp Ref Expression
1 a1i13.1 ⊢ ψ → θ
2 1 a1d ⊢ ψ → χ → θ
3 2 a1i ⊢ φ → ψ → χ → θ