Theorem reximdv 2928

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

Syntax hints:   -> wi 4   e. wcel 1823   E.wrex 2805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-ral 2809  df-rex 2810

This theorem is referenced by:  r19.12  2980  reusv3  4645  fvelima  5900  iunpw  6587  frxp  6883  ssfi  7733  ordtypelem2  7936  wdom2d  7998  xpwdomg  8003  cff1  8629  iunfo  8905  nqereu  9296  reclem3pr  9416  map2psrpr  9476  supsrlem  9477  1re  9584  exprelprel  12515  sswrdOLD  12545  o1lo1  13445  rlimcn1  13496  subcn2  13502  lo1add  13534  lo1mul  13535  pythagtriplem19  14444  vdwnnlem2  14601  ramub2  14619  sylow2alem2  16840  lsmless2x  16867  efgrelexlemb  16970  scmateALT  19184  decpmatmulsumfsupp  19444  pmatcollpw1lem1  19445  pmatcollpw2lem  19448  pm2mpmhmlem1  19489  cpmidpmatlem3  19543  cpmidgsum2  19550  tgcl  19641  neiss  19780  ssnei2  19787  tgcnp  19924  cnpco  19938  cnpresti  19959  lmcnp  19975  hausnei2  20024  1stcrest  20123  nlly2i  20146  llyss  20149  nllyss  20150  reftr  20184  lfinun  20195  txcnpi  20278  txcmplem1  20311  tx1stc  20320  nrmr0reg  20419  fbssfi  20507  fbfinnfr  20511  fgcl  20548  ufinffr  20599  elfm2  20618  fmfnfmlem1  20624  fmco  20631  fbflim2  20647  flffbas  20665  flftg  20666  cnpflf2  20670  alexsubALT  20720  cnextcn  20736  isucn2  20951  ucnima  20953  blssexps  21098  blssex  21099  mopni3  21166  neibl  21173  metss  21180  metcnp3  21212  cfilucfilOLD  21241  cfilucfil  21242  metustblOLD  21252  metustbl  21253  metutopOLD  21254  psmetutop  21255  rescncf  21570  lebnum  21633  xlebnum  21634  lebnumii  21635  lmmbr  21866  fgcfil  21879  ovolsslem  22064  ovolunlem1  22077  ovoliunnul  22087  itgcn  22418  ellimc3  22452  c1lip3  22569  itgsubstlem  22618  plyss  22765  ulmclm  22951  ulmcau  22959  ulmcn  22963  rlimcxp  23504  chtppilimlem2  23860  chtppilim  23861  midex  24315  usgranloop0  24585  usgra2edg  24587  3v3e3cycl1  24849  4cycl4v4e  24871  4cycl4dv4e  24873  vdusgra0nedg  25113  usgravd0nedg  25123  3cyclfrgrarn2  25219  vdn0frgrav2  25228  vdgn0frgrav2  25229  frgrawopreg1  25255  frgrawopreg2  25256  isgrpo  25399  opidonOLD  25525  rngmgmbs4  25620  xrge0infss  27814  tpr2rico  28132  esumpcvgval  28310  omssubadd  28511  conpcon  28947  cvmliftlem15  29010  cvmlift2lem10  29024  fnessref  30418  fdc1  30482  sstotbnd3  30515  totbndss  30516  heibor1lem  30548  heibor1  30549  fiphp3d  30995  pell1qrss14  31046  ssfiunibd  31751  infrglb  31826  climrec  31851  islptre  31867  lptre2pt  31888  ioodvbdlimc1lem2  31971  ioodvbdlimc2lem  31973  stoweidlem27  32051  stoweidlem29  32053  stoweidlem35  32059  stoweidlem48  32072  stoweidlem62  32086  fourierdlem48  32179  fourierdlem64  32195  fourierdlem65  32196  fourierdlem71  32202  fourierdlem73  32204  fourierdlem94  32225  fourierdlem103  32234  fourierdlem104  32235  fourierdlem112  32243  fourierdlem113  32244  afvelima  32494  usgvincvad  32795  usgvincvadALT  32798  pgrpgt2nabl  33232  lvoli2  35721  paddss2  35958  lhpexle1lem  36147  lhpexle2lem  36149  dvhdimlem  37587  dvh3dim3N  37592  mapdh9a  37933  hdmap11lem2  37988