Theorem reximdv 2915

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

Syntax hints:   -> wi 4   e. wcel 1802   E.wrex 2792

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1598  df-ral 2796  df-rex 2797

This theorem is referenced by:  r19.12  2967  reusv3  4642  fvelima  5907  iunpw  6596  frxp  6892  ssfi  7739  ordtypelem2  7944  wdom2d  8006  xpwdomg  8011  cff1  8638  iunfo  8914  nqereu  9307  reclem3pr  9427  map2psrpr  9487  supsrlem  9488  1re  9595  exprelprel  12504  sswrd  12531  o1lo1  13336  rlimcn1  13387  subcn2  13393  lo1add  13425  lo1mul  13426  pythagtriplem19  14231  vdwnnlem2  14388  ramub2  14406  sylow2alem2  16509  lsmless2x  16536  efgrelexlemb  16639  scmateALT  18884  decpmatmulsumfsupp  19144  pmatcollpw1lem1  19145  pmatcollpw2lem  19148  pm2mpmhmlem1  19189  cpmidpmatlem3  19243  cpmidgsum2  19250  tgcl  19341  neiss  19480  ssnei2  19487  tgcnp  19624  cnpco  19638  cnpresti  19659  lmcnp  19675  hausnei2  19724  1stcrest  19824  nlly2i  19847  llyss  19850  nllyss  19851  reftr  19885  lfinun  19896  txcnpi  19979  txcmplem1  20012  tx1stc  20021  nrmr0reg  20120  fbssfi  20208  fbfinnfr  20212  fgcl  20249  ufinffr  20300  elfm2  20319  fmfnfmlem1  20325  fmco  20332  fbflim2  20348  flffbas  20366  flftg  20367  cnpflf2  20371  alexsubALT  20421  cnextcn  20437  isucn2  20652  ucnima  20654  blssexps  20799  blssex  20800  mopni3  20867  neibl  20874  metss  20881  metcnp3  20913  cfilucfilOLD  20942  cfilucfil  20943  metustblOLD  20953  metustbl  20954  metutopOLD  20955  psmetutop  20956  rescncf  21271  lebnum  21334  xlebnum  21335  lebnumii  21336  lmmbr  21567  fgcfil  21580  ovolsslem  21765  ovolunlem1  21778  ovoliunnul  21788  itgcn  22119  ellimc3  22153  c1lip3  22270  itgsubstlem  22319  plyss  22466  ulmclm  22651  ulmcau  22659  ulmcn  22663  rlimcxp  23172  chtppilimlem2  23528  chtppilim  23529  midex  23980  usgranloop0  24249  usgra2edg  24251  3v3e3cycl1  24513  4cycl4v4e  24535  4cycl4dv4e  24537  vdusgra0nedg  24777  usgravd0nedg  24787  3cyclfrgrarn2  24883  vdn0frgrav2  24892  vdgn0frgrav2  24893  frgrawopreg1  24919  frgrawopreg2  24920  isgrpo  25067  opidonOLD  25193  rngmgmbs4  25288  xrge0infss  27449  tpr2rico  27764  esumpcvgval  27954  conpcon  28550  cvmliftlem15  28613  cvmlift2lem10  28627  fnessref  30147  fdc1  30211  sstotbnd3  30244  totbndss  30245  heibor1lem  30277  heibor1  30278  fiphp3d  30725  pell1qrss14  30776  ssfiunibd  31458  infrglb  31512  climrec  31517  islptre  31533  lptre2pt  31554  ioodvbdlimc1lem2  31633  ioodvbdlimc2lem  31635  stoweidlem27  31698  stoweidlem29  31700  stoweidlem35  31706  stoweidlem48  31719  stoweidlem62  31733  fourierdlem48  31826  fourierdlem64  31842  fourierdlem65  31843  fourierdlem71  31849  fourierdlem73  31851  fourierdlem94  31872  fourierdlem103  31881  fourierdlem104  31882  fourierdlem112  31890  fourierdlem113  31891  afvelima  32090  usgvincvad  32242  usgvincvadALT  32245  pgrpgt2nabl  32687  lvoli2  35028  paddss2  35265  lhpexle1lem  35454  lhpexle2lem  35456  dvhdimlem  36894  dvh3dim3N  36899  mapdh9a  37240  hdmap11lem2  37295