Theorem reximdv 2937

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

Syntax hints:   -> wi 4   e. wcel 1767   E.wrex 2815

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

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2819  df-rex 2820

This theorem is referenced by:  r19.12  2988  reusv3  4655  fvelima  5917  iunpw  6592  frxp  6890  ssfi  7737  ordtypelem2  7940  wdom2d  8002  xpwdomg  8007  cff1  8634  iunfo  8910  nqereu  9303  reclem3pr  9423  map2psrpr  9483  supsrlem  9484  1re  9591  exprelprel  12490  sswrd  12517  o1lo1  13319  rlimcn1  13370  subcn2  13376  lo1add  13408  lo1mul  13409  pythagtriplem19  14212  vdwnnlem2  14369  ramub2  14387  sylow2alem2  16434  lsmless2x  16461  efgrelexlemb  16564  scmateALT  18781  decpmatmulsumfsupp  19041  pmatcollpw1lem1  19042  pmatcollpw2lem  19045  pm2mpmhmlem1  19086  cpmidpmatlem3  19140  cpmidgsum2  19147  tgcl  19237  neiss  19376  ssnei2  19383  tgcnp  19520  cnpco  19534  cnpresti  19555  lmcnp  19571  hausnei2  19620  1stcrest  19720  nlly2i  19743  llyss  19746  nllyss  19747  txcnpi  19844  txcmplem1  19877  tx1stc  19886  nrmr0reg  19985  fbssfi  20073  fbfinnfr  20077  fgcl  20114  ufinffr  20165  elfm2  20184  fmfnfmlem1  20190  fmco  20197  fbflim2  20213  flffbas  20231  flftg  20232  cnpflf2  20236  alexsubALT  20286  cnextcn  20302  isucn2  20517  ucnima  20519  blssexps  20664  blssex  20665  mopni3  20732  neibl  20739  metss  20746  metcnp3  20778  cfilucfilOLD  20807  cfilucfil  20808  metustblOLD  20818  metustbl  20819  metutopOLD  20820  psmetutop  20821  rescncf  21136  lebnum  21199  xlebnum  21200  lebnumii  21201  lmmbr  21432  fgcfil  21445  ovolsslem  21630  ovolunlem1  21643  ovoliunnul  21653  itgcn  21984  ellimc3  22018  c1lip3  22135  itgsubstlem  22184  plyss  22331  ulmclm  22516  ulmcau  22524  ulmcn  22528  rlimcxp  23031  chtppilimlem2  23387  chtppilim  23388  mideu  23814  usgranloop0  24056  usgra2edg  24058  3v3e3cycl1  24320  4cycl4v4e  24342  4cycl4dv4e  24344  vdusgra0nedg  24584  usgravd0nedg  24594  3cyclfrgrarn2  24690  vdn0frgrav2  24700  vdgn0frgrav2  24701  frgrawopreg1  24727  frgrawopreg2  24728  isgrpo  24874  opidon  25000  rngmgmbs4  25095  xrge0infss  27248  tpr2rico  27530  esumpcvgval  27724  conpcon  28320  cvmliftlem15  28383  cvmlift2lem10  28397  reftr  29761  fnessref  29765  fdc1  29842  sstotbnd3  29875  totbndss  29876  heibor1lem  29908  heibor1  29909  fiphp3d  30357  pell1qrss14  30408  ssfiunibd  31086  infrglb  31140  climrec  31145  islptre  31161  lptre2pt  31182  stoweidlem27  31327  stoweidlem29  31329  stoweidlem35  31335  stoweidlem48  31348  stoweidlem62  31362  fourierdlem64  31471  fourierdlem65  31472  fourierdlem71  31478  fourierdlem73  31480  fourierdlem94  31501  fourierdlem103  31510  fourierdlem104  31511  fourierdlem112  31519  fourierdlem113  31520  afvelima  31719  usgvincvad  31873  usgvincvadALT  31876  pgrpgt2nabl  32024  lvoli2  34377  paddss2  34614  lhpexle1lem  34803  lhpexle2lem  34805  dvhdimlem  36241  dvh3dim3N  36246  mapdh9a  36587  hdmap11lem2  36642