Theorem 19.23 1411

Description: Theorem 19.23 of [Margaris] p. 90.

Hypothesis

Ref	Expression
19.23.1	|- (ps -> A.xps)

Assertion

Ref	Expression
19.23	|- (A.x(ph -> ps) <-> (E.xph -> ps))

Proof of Theorem 19.23

Step	Hyp	Ref	Expression
1		exim 1386	. . 3 |- (A.x(ph -> ps) -> (E.xph -> E.xps))
2		19.23.1	. . . 4 |- (ps -> A.xps)
3	2	19.9 1383	. . 3 |- (E.xps <-> ps)
4	1, 3	syl6ib 229	. 2 |- (A.x(ph -> ps) -> (E.xph -> ps))
5		hbe1 1363	. . . 4 |- (E.xph -> A.xE.xph)
6	5, 2	hbim 1354	. . 3 |- ((E.xph -> ps) -> A.x(E.xph -> ps))
7		19.8a 1376	. . . 4 |- (ph -> E.xph)
8	7	imim1i 19	. . 3 |- ((E.xph -> ps) -> (ph -> ps))
9	6, 8	19.21ai 1345	. 2 |- ((E.xph -> ps) -> A.x(ph -> ps))
10	4, 9	impbii 174	1 |- (A.x(ph -> ps) <-> (E.xph -> ps))

Syntax hints:   -> wi 3   <-> wb 163  A.wal 1296  E.wex 1326

This theorem is referenced by:  19.23ai 1412  19.23ad 1415  19.23t 1474  sbiedOLD 1564  19.23v 1672  r19.23 2206  r19.23OLD 2207  ceqsalgOLD 2315  r19.3rz 2960  ralidm 2973  euexeqOLD 3826  euexaleq 3827  bnj1035 12885  r19.3rzvb 14273  pm11.53 16344  ax10ext 16364  ax10-16 16365

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  ax-6o 1324

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

Copyright terms: Public domain