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