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	⊢ ( 𝜓 → ( 𝜒 → 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		2a1i.1	⊢ 𝜑
2	1	a1i	⊢ ( 𝜒 → 𝜑 )
3	2	a1i	⊢ ( 𝜓 → ( 𝜒 → 𝜑 ) )