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 φ ψ χ θ