Theorem 19.33bOLD 1445

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

Assertion

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

Proof of Theorem 19.33bOLD

Step	Hyp	Ref	Expression
1		ianor 329	. . . 4 |- (-. (E.xph /\ E.xps) <-> (-. E.xph \/ -. E.xps))
2		alnex 1380	. . . . 5 |- (A.x -. ph <-> -. E.xph)
3		alnex 1380	. . . . 5 |- (A.x -. ps <-> -. E.xps)
4	2, 3	orbi12i 277	. . . 4 |- ((A.x -. ph \/ A.x -. ps) <-> (-. E.xph \/ -. E.xps))
5	1, 4	bitr4i 193	. . 3 |- (-. (E.xph /\ E.xps) <-> (A.x -. ph \/ A.x -. ps))
6		biorf 807	. . . . . . 7 |- (-. ph -> (ps <-> (ph \/ ps)))
7	6	alimi 1338	. . . . . 6 |- (A.x -. ph -> A.x(ps <-> (ph \/ ps)))
8		albi 1344	. . . . . 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 290	. . . . 5 |- (A.xps -> (A.xph \/ A.xps))
11	9, 10	syl6bir 232	. . . 4 |- (A.x -. ph -> (A.x(ph \/ ps) -> (A.xph \/ A.xps)))
12		biorf 807	. . . . . . . 8 |- (-. ps -> (ph <-> (ps \/ ph)))
13		orcom 266	. . . . . . . 8 |- ((ps \/ ph) <-> (ph \/ ps))
14	12, 13	syl6bb 595	. . . . . . 7 |- (-. ps -> (ph <-> (ph \/ ps)))
15	14	alimi 1338	. . . . . 6 |- (A.x -. ps -> A.x(ph <-> (ph \/ ps)))
16		albi 1344	. . . . . 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 291	. . . . 5 |- (A.xph -> (A.xph \/ A.xps))
19	17, 18	syl6bir 232	. . . 4 |- (A.x -. ps -> (A.x(ph \/ ps) -> (A.xph \/ A.xps)))
20	11, 19	jaoi 368	. . 3 |- ((A.x -. ph \/ A.x -. ps) -> (A.x(ph \/ ps) -> (A.xph \/ A.xps)))
21	5, 20	sylbi 216	. 2 |- (-. (E.xph /\ E.xps) -> (A.x(ph \/ ps) -> (A.xph \/ A.xps)))
22		19.33 1443	. 2 |- ((A.xph \/ A.xps) -> A.x(ph \/ ps))
23	21, 22	impbid1 575	1 |- (-. (E.xph /\ E.xps) -> (A.x(ph \/ ps) <-> (A.xph \/ A.xps)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240  A.wal 1296  E.wex 1326

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327

Copyright terms: Public domain