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	$$⊢\phi$$
Assertion	2a1i	$$⊢\psi \to \left(\chi \to \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		2a1i.1	$$⊢\phi$$
2	1	a1i	$$⊢\chi \to \phi$$
3	2	a1i	$$⊢\psi \to \left(\chi \to \phi \right)$$