Theorem 19.33b 771

Description: The antecedent provides a condition implying the converse of 19.33 770. Compare Theorem 19.33 of [Margaris] p. 90.

Assertion

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

Proof of Theorem 19.33b

Step	Hyp	Ref	Expression
1		ianor 253	. . . 4 |- (-. (E.xph /\ E.xps) <-> (-. E.xph \/ -. E.xps))
2		alnex 716	. . . . 5 |- (A.x -. ph <-> -. E.xph)
3		alnex 716	. . . . 5 |- (A.x -. ps <-> -. E.xps)
4	2, 3	orbi12i 216	. . . 4 |- ((A.x -. ph \/ A.x -. ps) <-> (-. E.xph \/ -. E.xps))
5	1, 4	bitr4 154	. . 3 |- (-. (E.xph /\ E.xps) <-> (A.x -. ph \/ A.x -. ps))
6		biorf 551	. . . . . . 7 |- (-. ph -> (ps <-> (ph \/ ps)))
7	6	19.20i 691	. . . . . 6 |- (A.x -. ph -> A.x(ps <-> (ph \/ ps)))
8		19.15 694	. . . . . 6 |- (A.x(ps <-> (ph \/ ps)) -> (A.xps <-> A.x(ph \/ ps)))
9	7, 8	syl 12	. . . . 5 |- (A.x -. ph -> (A.xps <-> A.x(ph \/ ps)))
10		olc 224	. . . . 5 |- (A.xps -> (A.xph \/ A.xps))
11	9, 10	syl6bir 188	. . . 4 |- (A.x -. ph -> (A.x(ph \/ ps) -> (A.xph \/ A.xps)))
12		biorf 551	. . . . . . . 8 |- (-. ps -> (ph <-> (ps \/ ph)))
13		orcom 209	. . . . . . . 8 |- ((ps \/ ph) <-> (ph \/ ps))
14	12, 13	syl6bb 414	. . . . . . 7 |- (-. ps -> (ph <-> (ph \/ ps)))
15	14	19.20i 691	. . . . . 6 |- (A.x -. ps -> A.x(ph <-> (ph \/ ps)))
16		19.15 694	. . . . . 6 |- (A.x(ph <-> (ph \/ ps)) -> (A.xph <-> A.x(ph \/ ps)))
17	15, 16	syl 12	. . . . 5 |- (A.x -. ps -> (A.xph <-> A.x(ph \/ ps)))
18		orc 225	. . . . 5 |- (A.xph -> (A.xph \/ A.xps))
19	17, 18	syl6bir 188	. . . 4 |- (A.x -. ps -> (A.x(ph \/ ps) -> (A.xph \/ A.xps)))
20	11, 19	jaoi 275	. . 3 |- ((A.x -. ph \/ A.x -. ps) -> (A.x(ph \/ ps) -> (A.xph \/ A.xps)))
21	5, 20	sylbi 174	. 2 |- (-. (E.xph /\ E.xps) -> (A.x(ph \/ ps) -> (A.xph \/ A.xps)))
22		19.33 770	. . 3 |- ((A.xph \/ A.xps) -> A.x(ph \/ ps))
23	22	a1i 7	. 2 |- (-. (E.xph /\ E.xps) -> ((A.xph \/ A.xps) -> A.x(ph \/ ps)))
24	21, 23	impbid 397	1 |- (-. (E.xph /\ E.xps) -> (A.x(ph \/ ps) <-> (A.xph \/ A.xps)))

Syntax hints:  -. wn 1   -> wi 2   <-> wb 127   \/ wo 195   /\ wa 196  A.wal 672  E.wex 678

This theorem is referenced by:  kmlem16 3595

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679

metamath.org