Metamath Proof Explorer


Theorem a1i24

Description: Add two antecedents to a wff. Deduction associated with a1i13 . (Contributed by Jeff Hankins, 5-Aug-2009)

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

Proof

Step Hyp Ref Expression
1 a1i24.1 φ χ τ
2 1 a1dd φ χ θ τ
3 2 a1d φ ψ χ θ τ