Theorem 19.33b 1092

Description: The antecedent provides a condition implying the converse of 19.33 1091. 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 305	. . . 4 |- (-. (E.xph /\ E.xps) <-> (-. E.xph \/ -. E.xps))
2		alnex 1033	. . . . 5 |- (A.x -. ph <-> -. E.xph)
3		alnex 1033	. . . . 5 |- (A.x -. ps <-> -. E.xps)
4	2, 3	orbi12i 257	. . . 4 |- ((A.x -. ph \/ A.x -. ps) <-> (-. E.xph \/ -. E.xps))
5	1, 4	bitr4 176	. . 3 |- (-. (E.xph /\ E.xps) <-> (A.x -. ph \/ A.x -. ps))
6		biorf 735	. . . . . . 7 |- (-. ph -> (ps <-> (ph \/ ps)))
7	6	19.20i 992	. . . . . 6 |- (A.x -. ph -> A.x(ps <-> (ph \/ ps)))
8		19.15 997	. . . . . 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 268	. . . . 5 |- (A.xps -> (A.xph \/ A.xps))
11	9, 10	syl6bir 215	. . . 4 |- (A.x -. ph -> (A.x(ph \/ ps) -> (A.xph \/ A.xps)))
12		biorf 735	. . . . . . . 8 |- (-. ps -> (ph <-> (ps \/ ph)))
13		orcom 246	. . . . . . . 8 |- ((ps \/ ph) <-> (ph \/ ps))
14	12, 13	syl6bb 536	. . . . . . 7 |- (-. ps -> (ph <-> (ph \/ ps)))
15	14	19.20i 992	. . . . . 6 |- (A.x -. ps -> A.x(ph <-> (ph \/ ps)))
16		19.15 997	. . . . . 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 269	. . . . 5 |- (A.xph -> (A.xph \/ A.xps))
19	17, 18	syl6bir 215	. . . 4 |- (A.x -. ps -> (A.x(ph \/ ps) -> (A.xph \/ A.xps)))
20	11, 19	jaoi 341	. . 3 |- ((A.x -. ph \/ A.x -. ps) -> (A.x(ph \/ ps) -> (A.xph \/ A.xps)))
21	5, 20	sylbi 199	. 2 |- (-. (E.xph /\ E.xps) -> (A.x(ph \/ ps) -> (A.xph \/ A.xps)))
22		19.33 1091	. 2 |- ((A.xph \/ A.xps) -> A.x(ph \/ ps))
23	21, 22	impbid1 517	1 |- (-. (E.xph /\ E.xps) -> (A.x(ph \/ ps) <-> (A.xph \/ A.xps)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   \/ wo 222   /\ wa 223  A.wal 954  E.wex 980

This theorem is referenced by:  kmlem16 4780

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-4 973  ax-5o 975

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981

Copyright terms: Public domain