Theorem reximdv 2832

Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.) (Contributed by NM, 24-Jun-1998.)

Hypothesis

Ref	Expression
reximdv.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
reximdv	|- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)

Proof of Theorem reximdv

Step	Hyp	Ref	Expression
1		reximdv.1	. . 3 |- ( ph -> ( ps -> ch ) )
2	1	a1d 25	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	reximdvai 2831	1 |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

Syntax hints:   -> wi 4   e. wcel 1756   E.wrex 2721

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-ral 2725  df-rex 2726

This theorem is referenced by:  r19.12  2835  reusv3  4505  fvelima  5748  iunpw  6395  frxp  6687  ssfi  7538  ordtypelem2  7738  wdom2d  7800  xpwdomg  7805  cff1  8432  iunfo  8708  nqereu  9103  reclem3pr  9223  map2psrpr  9282  supsrlem  9283  1re  9390  sswrd  12247  o1lo1  13020  rlimcn1  13071  subcn2  13077  lo1add  13109  lo1mul  13110  pythagtriplem19  13905  vdwnnlem2  14062  ramub2  14080  sylow2alem2  16122  lsmless2x  16149  efgrelexlemb  16252  tgcl  18579  neiss  18718  ssnei2  18725  tgcnp  18862  cnpco  18876  cnpresti  18897  lmcnp  18913  hausnei2  18962  1stcrest  19062  nlly2i  19085  llyss  19088  nllyss  19089  txcnpi  19186  txcmplem1  19219  tx1stc  19228  nrmr0reg  19327  fbssfi  19415  fbfinnfr  19419  fgcl  19456  ufinffr  19507  elfm2  19526  fmfnfmlem1  19532  fmco  19539  fbflim2  19555  flffbas  19573  flftg  19574  cnpflf2  19578  alexsubALT  19628  cnextcn  19644  isucn2  19859  ucnima  19861  blssexps  20006  blssex  20007  mopni3  20074  neibl  20081  metss  20088  metcnp3  20120  cfilucfilOLD  20149  cfilucfil  20150  metustblOLD  20160  metustbl  20161  metutopOLD  20162  psmetutop  20163  rescncf  20478  lebnum  20541  xlebnum  20542  lebnumii  20543  lmmbr  20774  fgcfil  20787  ovolsslem  20972  ovolunlem1  20985  ovoliunnul  20995  itgcn  21325  ellimc3  21359  c1lip3  21476  itgsubstlem  21525  plyss  21672  ulmclm  21857  ulmcau  21865  ulmcn  21869  rlimcxp  22372  chtppilimlem2  22728  chtppilim  22729  usgranloop0  23304  usgra2edg  23306  3v3e3cycl1  23535  4cycl4v4e  23557  4cycl4dv4e  23559  vdusgra0nedg  23583  usgravd0nedg  23587  isgrpo  23688  opidon  23814  rngmgmbs4  23909  xrge0infss  26058  tpr2rico  26347  esumpcvgval  26532  conpcon  27129  cvmliftlem15  27192  cvmlift2lem10  27206  reftr  28566  fnessref  28570  fdc1  28647  sstotbnd3  28680  totbndss  28681  heibor1lem  28713  heibor1  28714  fiphp3d  29163  pell1qrss14  29214  infrglb  29776  climrec  29781  stoweidlem27  29827  stoweidlem29  29829  stoweidlem35  29835  stoweidlem48  29848  stoweidlem62  29862  afvelima  30078  exprelprel  30234  3cyclfrgrarn2  30611  vdn0frgrav2  30621  vdgn0frgrav2  30622  frgrawopreg1  30648  frgrawopreg2  30649  pgrpgt2nabel  30774  pmatcollpw2lem  30910  lvoli2  33230  paddss2  33467  lhpexle1lem  33656  lhpexle2lem  33658  dvhdimlem  35094  dvh3dim3N  35099  mapdh9a  35440  hdmap11lem2  35495