Theorem 19.41 1448

Description: Theorem 19.41 of [Margaris] p. 90. (The proof was shortened by Andrew Salmon, 25-May-2011.)

Hypothesis

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

Assertion

Ref	Expression
19.41	|- (E.x(ph /\ ps) <-> (E.xph /\ ps))

Proof of Theorem 19.41

Step	Hyp	Ref	Expression
1		19.40 1447	. . 3 |- (E.x(ph /\ ps) -> (E.xph /\ E.xps))
2		19.41.1	. . . . 5 |- (ps -> A.xps)
3		id 73	. . . . 5 |- (ps -> ps)
4	2, 3	19.23ai 1412	. . . 4 |- (E.xps -> ps)
5	4	anim2i 362	. . 3 |- ((E.xph /\ E.xps) -> (E.xph /\ ps))
6	1, 5	syl 12	. 2 |- (E.x(ph /\ ps) -> (E.xph /\ ps))
7		pm3.21 306	. . . 4 |- (ps -> (ph -> (ph /\ ps)))
8	2, 7	eximd 1410	. . 3 |- (ps -> (E.xph -> E.x(ph /\ ps)))
9	8	impcom 378	. 2 |- ((E.xph /\ ps) -> E.x(ph /\ ps))
10	6, 9	impbii 174	1 |- (E.x(ph /\ ps) <-> (E.xph /\ ps))

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

This theorem is referenced by:  19.42 1450  sbf 1551  hbs1fOLD 1556  19.41v 1685  eean 1706  euanOLD 1828  2euexOLD 1845  2exeu 1850  r19.41 2235  euobj1 3834  dfopab2 5053  dfoprab3 5054  bnj912 12822  bnj578 13291  bnj605 13292  bnj607 13304  bnj983 13357

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