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	|- ph
Assertion	2a1i	|- ( ps -> ( ch -> ph ) )

Proof

Step	Hyp	Ref	Expression
1		2a1i.1	|- ph
2	1	a1i	|- ( ch -> ph )
3	2	a1i	|- ( ps -> ( ch -> ph ) )