Metamath Proof Explorer


Theorem a1i14

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

Ref Expression
Hypothesis a1i14.1 ψ χ τ
Assertion a1i14 φ ψ χ θ τ

Proof

Step Hyp Ref Expression
1 a1i14.1 ψ χ τ
2 1 a1dd ψ χ θ τ
3 2 a1i φ ψ χ θ τ