Theorem 19.33b

Description: The antecedent provides a condition implying the converse of 19.33 . (Contributed by NM, 27-Mar-2004) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by Wolf Lammen, 5-Jul-2014)

	Ref	Expression
Assertion	19.33b	|- ( -. ( E. x ph /\ E. x ps ) -> ( A. x ( ph \/ ps ) <-> ( A. x ph \/ A. x ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		ianor	|- ( -. ( E. x ph /\ E. x ps ) <-> ( -. E. x ph \/ -. E. x ps ) )
2		alnex	|- ( A. x -. ph <-> -. E. x ph )
3		pm2.53	|- ( ( ph \/ ps ) -> ( -. ph -> ps ) )
4	3	al2imi	|- ( A. x ( ph \/ ps ) -> ( A. x -. ph -> A. x ps ) )
5	2 4	syl5bir	|- ( A. x ( ph \/ ps ) -> ( -. E. x ph -> A. x ps ) )
6		olc	|- ( A. x ps -> ( A. x ph \/ A. x ps ) )
7	5 6	syl6com	|- ( -. E. x ph -> ( A. x ( ph \/ ps ) -> ( A. x ph \/ A. x ps ) ) )
8		19.30	|- ( A. x ( ph \/ ps ) -> ( A. x ph \/ E. x ps ) )
9	8	orcomd	|- ( A. x ( ph \/ ps ) -> ( E. x ps \/ A. x ph ) )
10	9	ord	|- ( A. x ( ph \/ ps ) -> ( -. E. x ps -> A. x ph ) )
11		orc	|- ( A. x ph -> ( A. x ph \/ A. x ps ) )
12	10 11	syl6com	|- ( -. E. x ps -> ( A. x ( ph \/ ps ) -> ( A. x ph \/ A. x ps ) ) )
13	7 12	jaoi	|- ( ( -. E. x ph \/ -. E. x ps ) -> ( A. x ( ph \/ ps ) -> ( A. x ph \/ A. x ps ) ) )
14	1 13	sylbi	|- ( -. ( E. x ph /\ E. x ps ) -> ( A. x ( ph \/ ps ) -> ( A. x ph \/ A. x ps ) ) )
15		19.33	|- ( ( A. x ph \/ A. x ps ) -> A. x ( ph \/ ps ) )
16	14 15	impbid1	|- ( -. ( E. x ph /\ E. x ps ) -> ( A. x ( ph \/ ps ) <-> ( A. x ph \/ A. x ps ) ) )