Metamath Proof Explorer

Theorem 2a1i

Description: Inference introducing two antecedents. Two applications of a1i . Inference associated with 2a1 . (Contributed by Jeff Hankins, 4-Aug-2009)

Ref Expression
Hypothesis 2a1i.1 φ
Assertion 2a1i ψ χ φ


Step Hyp Ref Expression
1 2a1i.1 φ
2 1 a1i χ φ
3 2 a1i ψ χ φ