Theorem r19.23adva 1739

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version).

Hypothesis

Ref	Expression
r19.23adva.1	|- ((ph /\ x e. A) -> (ps -> ch))

Assertion

Ref	Expression
r19.23adva	|- (ph -> (E.x e. A ps -> ch))

Distinct variable groups:   ph,x   ch,x

Proof of Theorem r19.23adva

Step	Hyp	Ref	Expression
1		r19.23adva.1	. . 3 |- ((ph /\ x e. A) -> (ps -> ch))
2	1	ex 373	. 2 |- (ph -> (x e. A -> (ps -> ch)))
3	2	r19.23adv 1738	1 |- (ph -> (E.x e. A ps -> ch))

Syntax hints:   -> wi 3   /\ wa 223   e. wcel 955  E.wrex 1638

This theorem is referenced by:  r19.23aivv 1740  r19.23advv 1741  elunirnALT 3854  oawordexr 4174  oarec 4180  odi 4194  nneob 4239  onfin 4499  isfinite2 4523  cnegextlem1 5317  cnegextlem2 5318  cnegextlem3 5319  1re 5407  0re 5412  ioo0t 6305  sqr2irr 6659  seq1bnd 6847  infxpidmlem7 7501  infxpidmlem8 7502  infxpidmlem10 7504  tgclt 7566  subtop 7588  retopbas 7597  neindisj 7672  innei 7677  blssex 7794  metcnp 7826  lmle 7895  iscms2lem4 7926  bcthlem13 7945  ghgrpilem2 8071  nmobndi 8370  ubthlem5 8464  omlsi 9160  shsel3t 9194  spansncol 9407  nmopunt 9854  riesz1t 9913  hmopidmch 9990  cvcon3t 10121  chcv1t 10190  atcvatlem 10220  irred 10229

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-rex 1642

Copyright terms: Public domain