Theorem reximdv 2817

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

Syntax hints:   -> wi 4   e. wcel 1755   E.wrex 2706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-ral 2710  df-rex 2711

This theorem is referenced by:  r19.12  2820  reusv3  4488  fvelima  5731  iunpw  6379  frxp  6671  ssfi  7521  ordtypelem2  7721  wdom2d  7783  xpwdomg  7788  cff1  8415  iunfo  8691  nqereu  9085  reclem3pr  9205  map2psrpr  9264  supsrlem  9265  1re  9372  sswrd  12225  o1lo1  12998  rlimcn1  13049  subcn2  13055  lo1add  13087  lo1mul  13088  pythagtriplem19  13882  vdwnnlem2  14039  ramub2  14057  sylow2alem2  16096  lsmless2x  16123  efgrelexlemb  16226  tgcl  18415  neiss  18554  ssnei2  18561  tgcnp  18698  cnpco  18712  cnpresti  18733  lmcnp  18749  hausnei2  18798  1stcrest  18898  nlly2i  18921  llyss  18924  nllyss  18925  txcnpi  19022  txcmplem1  19055  tx1stc  19064  nrmr0reg  19163  fbssfi  19251  fbfinnfr  19255  fgcl  19292  ufinffr  19343  elfm2  19362  fmfnfmlem1  19368  fmco  19375  fbflim2  19391  flffbas  19409  flftg  19410  cnpflf2  19414  alexsubALT  19464  cnextcn  19480  isucn2  19695  ucnima  19697  blssexps  19842  blssex  19843  mopni3  19910  neibl  19917  metss  19924  metcnp3  19956  cfilucfilOLD  19985  cfilucfil  19986  metustblOLD  19996  metustbl  19997  metutopOLD  19998  psmetutop  19999  rescncf  20314  lebnum  20377  xlebnum  20378  lebnumii  20379  lmmbr  20610  fgcfil  20623  ovolsslem  20808  ovolunlem1  20821  ovoliunnul  20831  itgcn  21161  ellimc3  21195  c1lip3  21312  itgsubstlem  21361  plyss  21551  ulmclm  21736  ulmcau  21744  ulmcn  21748  rlimcxp  22251  chtppilimlem2  22607  chtppilim  22608  usgranloop0  23121  usgra2edg  23123  3v3e3cycl1  23352  4cycl4v4e  23374  4cycl4dv4e  23376  vdusgra0nedg  23400  usgravd0nedg  23404  isgrpo  23505  opidon  23631  rngmgmbs4  23726  tpr2rico  26195  esumpcvgval  26380  conpcon  26971  cvmliftlem15  27034  cvmlift2lem10  27048  reftr  28402  fnessref  28406  fdc1  28483  sstotbnd3  28516  totbndss  28517  heibor1lem  28549  heibor1  28550  fiphp3d  29000  pell1qrss14  29051  infrglb  29614  climrec  29619  stoweidlem27  29665  stoweidlem29  29667  stoweidlem35  29673  stoweidlem48  29686  stoweidlem62  29700  afvelima  29916  exprelprel  30072  3cyclfrgrarn2  30449  vdn0frgrav2  30459  vdgn0frgrav2  30460  frgrawopreg1  30486  frgrawopreg2  30487  pgrpgt2nabel  30597  lvoli2  32795  paddss2  33032  lhpexle1lem  33221  lhpexle2lem  33223  dvhdimlem  34659  dvh3dim3N  34664  mapdh9a  35005  hdmap11lem2  35060