Theorem 19.33b 1133

Description: The antecedent provides a condition implying the converse of 19.33 1132. 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 312	. . . 4 |- (-. (E.xph /\ E.xps) <-> (-. E.xph \/ -. E.xps))
2		alnex 1074	. . . . 5 |- (A.x -. ph <-> -. E.xph)
3		alnex 1074	. . . . 5 |- (A.x -. ps <-> -. E.xps)
4	2, 3	orbi12i 264	. . . 4 |- ((A.x -. ph \/ A.x -. ps) <-> (-. E.xph \/ -. E.xps))
5	1, 4	bitr4i 183	. . 3 |- (-. (E.xph /\ E.xps) <-> (A.x -. ph \/ A.x -. ps))
6		biorf 747	. . . . . . 7 |- (-. ph -> (ps <-> (ph \/ ps)))
7	6	19.20i 1033	. . . . . 6 |- (A.x -. ph -> A.x(ps <-> (ph \/ ps)))
8		19.15 1038	. . . . . 6 |- (A.x(ps <-> (ph \/ ps)) -> (A.xps <-> A.x(ph \/ ps)))
9	7, 8	syl 10	. . . . 5 |- (A.x -. ph -> (A.xps <-> A.x(ph \/ ps)))
10		olc 275	. . . . 5 |- (A.xps -> (A.xph \/ A.xps))
11	9, 10	syl6bir 222	. . . 4 |- (A.x -. ph -> (A.x(ph \/ ps) -> (A.xph \/ A.xps)))
12		biorf 747	. . . . . . . 8 |- (-. ps -> (ph <-> (ps \/ ph)))
13		orcom 253	. . . . . . . 8 |- ((ps \/ ph) <-> (ph \/ ps))
14	12, 13	syl6bb 547	. . . . . . 7 |- (-. ps -> (ph <-> (ph \/ ps)))
15	14	19.20i 1033	. . . . . 6 |- (A.x -. ps -> A.x(ph <-> (ph \/ ps)))
16		19.15 1038	. . . . . 6 |- (A.x(ph <-> (ph \/ ps)) -> (A.xph <-> A.x(ph \/ ps)))
17	15, 16	syl 10	. . . . 5 |- (A.x -. ps -> (A.xph <-> A.x(ph \/ ps)))
18		orc 276	. . . . 5 |- (A.xph -> (A.xph \/ A.xps))
19	17, 18	syl6bir 222	. . . 4 |- (A.x -. ps -> (A.x(ph \/ ps) -> (A.xph \/ A.xps)))
20	11, 19	jaoi 348	. . 3 |- ((A.x -. ph \/ A.x -. ps) -> (A.x(ph \/ ps) -> (A.xph \/ A.xps)))
21	5, 20	sylbi 206	. 2 |- (-. (E.xph /\ E.xps) -> (A.x(ph \/ ps) -> (A.xph \/ A.xps)))
22		19.33 1132	. 2 |- ((A.xph \/ A.xps) -> A.x(ph \/ ps))
23	21, 22	impbid1 528	1 |- (-. (E.xph /\ E.xps) -> (A.x(ph \/ ps) <-> (A.xph \/ A.xps)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 153   \/ wo 229   /\ wa 230  A.wal 995  E.wex 1021

This theorem is referenced by:  kmlem16 4842

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-4 1014  ax-5o 1016

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022

Copyright terms: Public domain