Theorem reximdv 3170

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
ralimdv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
reximdv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reximdv

Step	Hyp	Ref	Expression
1		ralimdv.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	a1d 25	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	reximdvai 3165	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2108  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3071

This theorem is referenced by:  r19.12  3314  r19.12OLD  3315  ss2rexv  4055  reusv3  5405  fvelima  6974  iunpw  7791  frxp  8151  nnaordex2  8677  ssfiALT  9214  ordtypelem2  9559  wdom2d  9620  xpwdomg  9625  cff1  10298  iunfo  10579  nqereu  10969  reclem3pr  11089  map2psrpr  11150  supsrlem  11151  1re  11261  elss2prb  14527  exprelprel  14529  o1lo1  15573  rlimcn1  15624  subcn2  15631  lo1add  15663  lo1mul  15664  pythagtriplem19  16871  vdwnnlem2  17034  ramub2  17052  sylow2alem2  19636  lsmless2x  19663  efgrelexlemb  19768  scmateALT  22518  decpmatmulsumfsupp  22779  pmatcollpw1lem1  22780  pmatcollpw2lem  22783  pm2mpmhmlem1  22824  cpmidpmatlem3  22878  cpmidgsum2  22885  tgcl  22976  neiss  23117  ssnei2  23124  tgcnp  23261  cnpco  23275  cnpresti  23296  lmcnp  23312  hausnei2  23361  1stcrest  23461  nlly2i  23484  llyss  23487  nllyss  23488  reftr  23522  lfinun  23533  txcnpi  23616  txcmplem1  23649  tx1stc  23658  nrmr0reg  23757  fbssfi  23845  fbfinnfr  23849  fgcl  23886  ufinffr  23937  elfm2  23956  fmfnfmlem1  23962  fmco  23969  fbflim2  23985  flffbas  24003  flftg  24004  cnpflf2  24008  alexsubALT  24059  cnextcn  24075  isucn2  24288  ucnima  24290  blssexps  24436  blssex  24437  mopni3  24507  neibl  24514  metss  24521  metcnp3  24553  cfilucfil  24572  metustbl  24579  psmetutop  24580  mpomulcn  24891  rescncf  24923  lebnum  24996  xlebnum  24997  lebnumii  24998  lmmbr  25292  fgcfil  25305  ovolsslem  25519  ovolunlem1  25532  ovoliunnul  25542  itgcn  25880  ellimc3  25914  c1lip3  26038  itgsubstlem  26089  plyss  26238  ulmclm  26430  ulmcau  26438  ulmcn  26442  rlimcxp  27017  chtppilimlem2  27518  chtppilim  27519  madess  27915  lrrecfr  27976  midex  28745  umgrnloop0  29126  usgrnloop0ALT  29222  uhgr2edg  29225  vtxduhgr0nedg  29510  wlkonl1iedg  29683  elwspths2on  29980  3cyclfrgrrn2  30306  isgrpo  30516  tpr2rico  33911  esumpcvgval  34079  omssubadd  34302  connpconn  35240  cvmliftlem15  35303  cvmlift2lem10  35317  satfdmlem  35373  fmla1  35392  satffunlem1lem2  35408  satffunlem2lem2  35411  fnessref  36358  fvineqsneq  37413  pibt2  37418  ptrecube  37627  poimirlem29  37656  poimirlem30  37657  poimirlem31  37658  fdc1  37753  sstotbnd3  37783  totbndss  37784  heibor1lem  37816  heibor1  37817  opidonOLD  37859  rngmgmbs4  37938  lvoli2  39583  paddss2  39820  lhpexle1lem  40009  lhpexle2lem  40011  dvhdimlem  41446  dvh3dim3N  41451  mapdh9a  41791  hdmap11lem2  41844  fiphp3d  42830  pell1qrss14  42879  minregex  43547  mnuop3d  44290  grumnudlem  44304  ismnushort  44320  eliuniin  45104  restuni3  45123  eliuniin2  45125  disjrnmpt2  45193  rnmptbd2lem  45255  ssfiunibd  45321  supminfxrrnmpt  45482  climrec  45618  islptre  45634  lptre2pt  45655  limsupmnfuzlem  45741  limsupre3lem  45747  limsupvaluz2  45753  supcnvlimsup  45755  liminfvalxr  45798  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  stoweidlem27  46042  stoweidlem29  46044  stoweidlem35  46050  stoweidlem48  46063  stoweidlem62  46077  fourierdlem48  46169  fourierdlem64  46185  fourierdlem65  46186  fourierdlem71  46192  fourierdlem73  46194  fourierdlem94  46215  fourierdlem103  46224  fourierdlem104  46225  fourierdlem112  46233  fourierdlem113  46234  sge0isum  46442  sge0seq  46461  meaiuninclem  46495  carageniuncllem2  46537  ovnsslelem  46575  hoidmvlelem1  46610  2reuimp  47127  afvelima  47179  sgoldbeven3prm  47770  nnsum4primes4  47776  nnsum4primesprm  47778  nnsum4primesgbe  47780  nnsum4primesle9  47782  grtriprop  47908  pgrpgt2nabl  48282  opnneilv  48806  sepnsepo  48821