Theorem pm10.56

Description: Theorem *10.56 in WhiteheadRussell p. 156. (Contributed by Andrew Salmon, 24-May-2011)

	Ref	Expression
Assertion	pm10.56	|- ( ( A. x ( ph -> ps ) /\ E. x ( ph /\ ch ) ) -> E. x ( ps /\ ch ) )

Proof

Step	Hyp	Ref	Expression
1		pm3.45	|- ( ( ph -> ps ) -> ( ( ph /\ ch ) -> ( ps /\ ch ) ) )
2	1	aleximi	|- ( A. x ( ph -> ps ) -> ( E. x ( ph /\ ch ) -> E. x ( ps /\ ch ) ) )
3	2	imp	|- ( ( A. x ( ph -> ps ) /\ E. x ( ph /\ ch ) ) -> E. x ( ps /\ ch ) )