Theorem pm10.57

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

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

Proof

Step	Hyp	Ref	Expression
1		alnex	|- ( A. x -. ( ph /\ ch ) <-> -. E. x ( ph /\ ch ) )
2		imnan	|- ( ( ph -> -. ch ) <-> -. ( ph /\ ch ) )
3		pm2.53	|- ( ( ps \/ ch ) -> ( -. ps -> ch ) )
4	3	con1d	|- ( ( ps \/ ch ) -> ( -. ch -> ps ) )
5	4	imim3i	|- ( ( ph -> ( ps \/ ch ) ) -> ( ( ph -> -. ch ) -> ( ph -> ps ) ) )
6	2 5	syl5bir	|- ( ( ph -> ( ps \/ ch ) ) -> ( -. ( ph /\ ch ) -> ( ph -> ps ) ) )
7	6	al2imi	|- ( A. x ( ph -> ( ps \/ ch ) ) -> ( A. x -. ( ph /\ ch ) -> A. x ( ph -> ps ) ) )
8	1 7	syl5bir	|- ( A. x ( ph -> ( ps \/ ch ) ) -> ( -. E. x ( ph /\ ch ) -> A. x ( ph -> ps ) ) )
9	8	con1d	|- ( A. x ( ph -> ( ps \/ ch ) ) -> ( -. A. x ( ph -> ps ) -> E. x ( ph /\ ch ) ) )
10	9	orrd	|- ( A. x ( ph -> ( ps \/ ch ) ) -> ( A. x ( ph -> ps ) \/ E. x ( ph /\ ch ) ) )