Theorem reximdv 2873

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 26	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	reximdvai 2871	1 |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

Syntax hints:   -> wi 4   e. wcel 1898   E.wrex 2750

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-ral 2754  df-rex 2755

This theorem is referenced by:  r19.12  2928  reusv3  4625  fvelima  5940  iunpw  6632  frxp  6933  ssfi  7818  ordtypelem2  8060  wdom2d  8121  xpwdomg  8126  cff1  8714  iunfo  8990  nqereu  9380  reclem3pr  9500  map2psrpr  9560  supsrlem  9561  1re  9668  elss2prb  12676  exprelprel  12679  sswrdOLD  12713  o1lo1  13650  rlimcn1  13701  subcn2  13707  lo1add  13739  lo1mul  13740  pythagtriplem19  14832  vdwnnlem2  14995  ramub2  15020  sylow2alem2  17319  lsmless2x  17346  efgrelexlemb  17449  scmateALT  19586  decpmatmulsumfsupp  19846  pmatcollpw1lem1  19847  pmatcollpw2lem  19850  pm2mpmhmlem1  19891  cpmidpmatlem3  19945  cpmidgsum2  19952  tgcl  20034  neiss  20174  ssnei2  20181  tgcnp  20318  cnpco  20332  cnpresti  20353  lmcnp  20369  hausnei2  20418  1stcrest  20517  nlly2i  20540  llyss  20543  nllyss  20544  reftr  20578  lfinun  20589  txcnpi  20672  txcmplem1  20705  tx1stc  20714  nrmr0reg  20813  fbssfi  20901  fbfinnfr  20905  fgcl  20942  ufinffr  20993  elfm2  21012  fmfnfmlem1  21018  fmco  21025  fbflim2  21041  flffbas  21059  flftg  21060  cnpflf2  21064  alexsubALT  21115  cnextcn  21131  isucn2  21343  ucnima  21345  blssexps  21490  blssex  21491  mopni3  21558  neibl  21565  metss  21572  metcnp3  21604  cfilucfil  21623  metustbl  21630  psmetutop  21631  rescncf  21978  lebnum  22044  xlebnum  22045  lebnumii  22046  lmmbr  22277  fgcfil  22290  ovolsslem  22486  ovolunlem1  22499  ovoliunnul  22509  itgcn  22849  ellimc3  22883  c1lip3  23000  itgsubstlem  23049  plyss  23202  ulmclm  23391  ulmcau  23399  ulmcn  23403  rlimcxp  23948  chtppilimlem2  24361  chtppilim  24362  midex  24828  usgranloop0  25156  usgra2edg  25158  3v3e3cycl1  25421  4cycl4v4e  25443  4cycl4dv4e  25445  vdusgra0nedg  25685  usgravd0nedg  25695  3cyclfrgrarn2  25791  vdn0frgrav2  25800  vdgn0frgrav2  25801  frgrawopreg1  25827  frgrawopreg2  25828  isgrpo  25973  opidonOLD  26099  rngmgmbs4  26194  xrge0infssOLD  28390  tpr2rico  28767  esumpcvgval  28948  omssubadd  29177  omssubaddOLD  29181  conpcon  30007  cvmliftlem15  30070  cvmlift2lem10  30084  fnessref  31062  ptrecube  31985  poimirlem29  32014  poimirlem30  32015  poimirlem31  32016  fdc1  32120  sstotbnd3  32153  totbndss  32154  heibor1lem  32186  heibor1  32187  lvoli2  33191  paddss2  33428  lhpexle1lem  33617  lhpexle2lem  33619  dvhdimlem  35057  dvh3dim3N  35062  mapdh9a  35403  hdmap11lem2  35458  fiphp3d  35707  pell1qrss14  35759  disjrnmpt2  37501  ssfiunibd  37565  infrglbOLD  37707  climrec  37719  islptre  37737  lptre2pt  37758  ioodvbdlimc1lem2  37842  ioodvbdlimc1lem2OLD  37844  ioodvbdlimc2lem  37846  ioodvbdlimc2lemOLD  37847  stoweidlem27  37925  stoweidlem29  37927  stoweidlem29OLD  37928  stoweidlem35  37934  stoweidlem48  37947  stoweidlem62  37961  stoweidlem62OLD  37962  fourierdlem48  38056  fourierdlem64  38072  fourierdlem65  38073  fourierdlem71  38079  fourierdlem73  38081  fourierdlem94  38102  fourierdlem103  38111  fourierdlem104  38112  fourierdlem112  38120  fourierdlem113  38121  sge0isum  38307  carageniuncllem2  38381  ovnsslelem  38420  hoidmvlelem1  38455  afvelima  38707  nnsum4primes4  38922  nnsum4primesprm  38924  nnsum4primesgbe  38926  nnsum4primesle9  38928  umgrnloop0  39245  usgrnloop0ALT  39336  uhgr2edg  39339  vtxduhgr0nedg  39596  usgvincvad  39989  usgvincvadALT  39992  pgrpgt2nabl  40424