Theorem reximdv 2906

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 2904	1 |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

Syntax hints:   -> wi 4   e. wcel 1870   E.wrex 2783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-ral 2787  df-rex 2788

This theorem is referenced by:  r19.12  2961  reusv3  4633  fvelima  5933  iunpw  6619  frxp  6917  ssfi  7798  ordtypelem2  8034  wdom2d  8095  xpwdomg  8100  cff1  8686  iunfo  8962  nqereu  9353  reclem3pr  9473  map2psrpr  9533  supsrlem  9534  1re  9641  exprelprel  12637  sswrdOLD  12667  o1lo1  13579  rlimcn1  13630  subcn2  13636  lo1add  13668  lo1mul  13669  pythagtriplem19  14746  vdwnnlem2  14909  ramub2  14934  sylow2alem2  17205  lsmless2x  17232  efgrelexlemb  17335  scmateALT  19468  decpmatmulsumfsupp  19728  pmatcollpw1lem1  19729  pmatcollpw2lem  19732  pm2mpmhmlem1  19773  cpmidpmatlem3  19827  cpmidgsum2  19834  tgcl  19916  neiss  20056  ssnei2  20063  tgcnp  20200  cnpco  20214  cnpresti  20235  lmcnp  20251  hausnei2  20300  1stcrest  20399  nlly2i  20422  llyss  20425  nllyss  20426  reftr  20460  lfinun  20471  txcnpi  20554  txcmplem1  20587  tx1stc  20596  nrmr0reg  20695  fbssfi  20783  fbfinnfr  20787  fgcl  20824  ufinffr  20875  elfm2  20894  fmfnfmlem1  20900  fmco  20907  fbflim2  20923  flffbas  20941  flftg  20942  cnpflf2  20946  alexsubALT  20997  cnextcn  21013  isucn2  21225  ucnima  21227  blssexps  21372  blssex  21373  mopni3  21440  neibl  21447  metss  21454  metcnp3  21486  cfilucfil  21505  metustbl  21512  psmetutop  21513  rescncf  21825  lebnum  21888  xlebnum  21889  lebnumii  21890  lmmbr  22121  fgcfil  22134  ovolsslem  22315  ovolunlem1  22328  ovoliunnul  22338  itgcn  22677  ellimc3  22711  c1lip3  22828  itgsubstlem  22877  plyss  23021  ulmclm  23207  ulmcau  23215  ulmcn  23219  rlimcxp  23764  chtppilimlem2  24175  chtppilim  24176  midex  24636  usgranloop0  24953  usgra2edg  24955  3v3e3cycl1  25217  4cycl4v4e  25239  4cycl4dv4e  25241  vdusgra0nedg  25481  usgravd0nedg  25491  3cyclfrgrarn2  25587  vdn0frgrav2  25596  vdgn0frgrav2  25597  frgrawopreg1  25623  frgrawopreg2  25624  isgrpo  25769  opidonOLD  25895  rngmgmbs4  25990  xrge0infss  28181  tpr2rico  28557  esumpcvgval  28738  omssubadd  28961  conpcon  29746  cvmliftlem15  29809  cvmlift2lem10  29823  fnessref  30798  ptrecube  31644  poimirlem29  31673  poimirlem30  31674  poimirlem31  31675  fdc1  31779  sstotbnd3  31812  totbndss  31813  heibor1lem  31845  heibor1  31846  lvoli2  32855  paddss2  33092  lhpexle1lem  33281  lhpexle2lem  33283  dvhdimlem  34721  dvh3dim3N  34726  mapdh9a  35067  hdmap11lem2  35122  fiphp3d  35371  pell1qrss14  35422  disjrnmpt2  37086  ssfiunibd  37136  infrglbOLD  37241  climrec  37253  islptre  37271  lptre2pt  37292  ioodvbdlimc1lem2  37376  ioodvbdlimc2lem  37378  stoweidlem27  37456  stoweidlem29  37458  stoweidlem29OLD  37459  stoweidlem35  37465  stoweidlem48  37478  stoweidlem62  37492  stoweidlem62OLD  37493  fourierdlem48  37586  fourierdlem64  37602  fourierdlem65  37603  fourierdlem71  37609  fourierdlem73  37611  fourierdlem94  37632  fourierdlem103  37641  fourierdlem104  37642  fourierdlem112  37650  fourierdlem113  37651  carageniuncllem2  37852  afvelima  38059  nnsum4primes4  38274  nnsum4primesprm  38276  nnsum4primesgbe  38278  nnsum4primesle9  38280  usgvincvad  38474  usgvincvadALT  38477  pgrpgt2nabl  38911