Theorem bnj1023

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1023.1	|- E. x ( ph -> ps )
	bnj1023.2	|- ( ps -> ch )
Assertion	bnj1023	|- E. x ( ph -> ch )

Proof

Step	Hyp	Ref	Expression
1		bnj1023.1	|- E. x ( ph -> ps )
2		bnj1023.2	|- ( ps -> ch )
3	2	a1i	|- ( ( ph -> ps ) -> ( ps -> ch ) )
4	3	ax-gen	|- A. x ( ( ph -> ps ) -> ( ps -> ch ) )
5		exintr	|- ( A. x ( ( ph -> ps ) -> ( ps -> ch ) ) -> ( E. x ( ph -> ps ) -> E. x ( ( ph -> ps ) /\ ( ps -> ch ) ) ) )
6	4 1 5	mp2	|- E. x ( ( ph -> ps ) /\ ( ps -> ch ) )
7		pm3.33	|- ( ( ( ph -> ps ) /\ ( ps -> ch ) ) -> ( ph -> ch ) )
8	6 7	bnj101	|- E. x ( ph -> ch )