Theorem reximdva 3174

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)

Hypothesis

Ref	Expression
ralimdva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))

Assertion

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

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem reximdva

Step	Hyp	Ref	Expression
1		ralimdva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
2	1	ex 412	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	reximdvai 3171	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  reximddv  3177  reximdvva  3213  reximddv2  3221  wereu2  5697  frpomin  6372  dffo4  7137  nnaordex  8694  frfi  9349  fisupg  9352  marypha1  9503  fiinfg  9568  wemapsolem  9619  unwdomg  9653  rankr1ai  9867  cofsmo  10338  cfcoflem  10341  inar1  10844  nqerf  10999  prlem936  11116  fimaxre  12239  fiminre  12242  arch  12550  bndndx  12552  suprfinzcl  12757  zmin  13009  elpq  13040  qbtwnxr  13262  qsqueeze  13263  qextltlem  13264  xrsupsslem  13369  xrinfmsslem  13370  xrub  13374  supxrunb1  13381  ssnn0fi  14036  fsuppmapnn0fiub0  14044  fsuppmapnn0fz  14047  expnlbnd2  14283  r19.29uz  15399  cau3lem  15403  rlim2lt  15543  rlimclim  15592  2clim  15618  o1co  15632  climcn1  15638  climcn2  15639  rlimo1  15663  climsqz  15687  climsqz2  15688  rlimsqzlem  15697  lo1le  15700  climsup  15718  climcau  15719  caucvgrlem2  15723  iseralt  15733  cvgcmp  15864  cvgcmpce  15866  supcvg  15904  rpnnen2lem12  16273  bezoutlem1  16586  divgcdcoprmex  16713  exprmfct  16751  prmdvdsfz  16752  prmdvdsncoprmbd  16774  pclem  16885  pc2dvds  16926  pcprmpw  16930  dvdsprmpweqle  16933  unbenlem  16955  infpnlem2  16958  infpn2  16960  prmunb  16961  vdwlem2  17029  ramub1lem2  17074  prmdvdsprmop  17090  prmgaplem7  17104  ipodrsima  18611  smndex1mgm  18942  grpinveu  19014  dfgrp3lem  19078  psgneu  19548  odbezout  19600  sylow2blem3  19664  nn0gsumfz  20026  irredrmul  20453  zrninitoringc  20698  lbsextlem2  21184  znunit  21605  mptcoe1fsupp  22238  evls1fpws  22394  scmate  22537  scmatscm  22540  scmatfo  22557  mat1scmat  22566  pmatcoe1fsupp  22728  pmatcollpwfi  22809  pmatcollpw3fi  22812  mptcoe1matfsupp  22829  pm2mp  22852  chmaidscmat  22875  cpmadumatpoly  22910  chcoeffeq  22913  cayhamlem3  22914  cayhamlem4  22915  neiptopnei  23161  neitr  23209  cnpnei  23293  haust1  23381  isnrm3  23388  isreg2  23406  tgcmp  23430  hauscmplem  23435  hauscmp  23436  bwth  23439  1stcfb  23474  1stcelcls  23490  lly1stc  23525  txcmplem1  23670  txlm  23677  xkococnlem  23688  filuni  23914  filufint  23949  ufilen  23959  fclscf  24054  cnextcn  24096  ustex2sym  24246  ustex3sym  24247  utopreg  24282  isucn2  24309  ucnima  24311  ucncn  24315  neipcfilu  24326  metequiv2  24544  metrest  24558  xrsmopn  24853  mulc1cncf  24950  cncfco  24952  bndth  25009  lmmcvg  25314  cfil3i  25322  iscau4  25332  cmetcaulem  25341  iscmet3lem1  25344  caussi  25350  equivcfil  25352  equivcau  25353  caubl  25361  minveclem3b  25481  ovolgelb  25534  ovollb2lem  25542  ovolctb  25544  ovolicc2lem4  25574  ioombl1lem4  25615  dyadmax  25652  volsup2  25659  itg2monolem1  25805  c1liplem1  26055  c1lip1  26056  dvivthlem1  26067  lhop1  26073  ftc1a  26098  ftc1lem6  26102  ply1divex  26196  elply2  26255  dgrlem  26288  aacjcl  26387  aalioulem2  26393  aalioulem3  26394  aalioulem4  26395  ulmcaulem  26455  ulmcau  26456  ulmss  26458  mtest  26465  itgulm  26469  reeff1o  26509  efif1olem4  26605  rlimcnp  27026  xrlimcnp  27029  lgamucov  27099  ftalem3  27136  fta  27141  muval1  27194  dvdssqf  27199  mumullem1  27240  lgsqrmod  27414  lgsqrmodndvds  27415  pntlem3  27671  ostth  27701  nosupno  27766  nosupbnd1lem4  27774  noinfno  27781  noinfbnd1lem4  27789  conway  27862  etasslt  27876  znegscl  28396  tgtrisegint  28525  tgbtwndiff  28532  tgcgrxfr  28544  lnext  28593  legov2  28612  legtrd  28615  hlcgrex  28642  colperpexlem3  28758  colperpex  28759  hlpasch  28782  hpgerlem  28791  hpgtr  28794  dfcgra2  28856  acopy  28859  inagswap  28867  inaghl  28871  cgrg3col4  28879  axpasch  28974  wwlksnredwwlkn0  29929  midwwlks2s3  29985  clwwlkn1loopb  30075  2pthfrgrrn2  30315  frgrwopreg1  30350  frgrwopreg2  30351  grpoidinvlem3  30538  grpoideu  30541  grpoinveu  30551  ubthlem1  30902  minvecolem5  30913  htthlem  30949  chscllem2  31670  nmopun  32046  lnconi  32065  rnbra  32139  sumdmdii  32447  cdj3lem2b  32469  foresf1o  32532  acunirnmpt  32677  xrofsup  32774  fprodex01  32829  mndlactfo  33013  mndractfo  33015  isarchi3  33167  erler  33237  isarchiofld  33312  dfufd2lem  33542  constrconj  33735  lmxrge0  33898  lmdvg  33899  esumlub  34024  esumfsup  34034  esumcvg  34050  ftc2re  34575  cusgr3cyclex  35104  cvmliftmolem2  35250  cvmlift2lem12  35282  satfv1  35331  satffunlem1lem2  35371  satffunlem2lem2  35374  satfv0fvfmla0  35381  ellcsrspsn  35609  r1peuqusdeg1  35611  wzel  35788  wsuclem  35789  btwndiff  35991  trisegint  35992  cgrxfr  36019  lineext  36040  segcon2  36069  brsegle2  36073  seglecgr12im  36074  segletr  36078  broutsideof3  36090  opnrebl2  36287  nn0prpw  36289  fin2so  37567  poimirlem27  37607  poimirlem30  37610  poimirlem31  37611  poimir  37613  mblfinlem1  37617  mblfinlem2  37618  mblfinlem3  37619  mblfinlem4  37620  itg2addnclem  37631  ftc1cnnc  37652  ftc1anclem5  37657  sdclem1  37703  geomcau  37719  equivtotbnd  37738  bndss  37746  ismtybndlem  37766  heibor1lem  37769  rrncmslem  37792  rngo2  37867  prtlem15  38831  lsateln0  38951  lsat0cv  38989  eqlkr3  39057  lkrshp  39061  lshpset2N  39075  hlhgt2  39346  hlrelat2  39360  atle  39393  athgt  39413  2dim  39427  1cvratex  39430  ps-2  39435  dalem20  39650  lhpexle1lem  39964  lhpexle1  39965  lhpexle2lem  39966  lhpmcvr5N  39984  lhpmcvr6N  39985  cdleme25a  40310  cdleme29ex  40331  cdlemfnid  40521  cdlemg33b0  40658  cdlemg33a  40663  cdlemg35  40670  cdleml3N  40935  dihlsscpre  41191  dih1dimb2  41198  dihatexv  41295  dvh3dim2  41405  dochkr1  41435  dochkr1OLDN  41436  lcfl8  41459  lcfl8b  41461  lcfrlem5  41503  lcfrlem6  41504  mapdrvallem2  41602  mapdh9a  41746  mapdh9aOLDN  41747  hdmaprnlem3eN  41815  hdmaprnlem16N  41819  mndmolinv  42052  primrootsunit1  42054  flt4lem5elem  42606  flt4lem7  42614  nna4b4nsq  42615  fphpdo  42773  rencldnfilem  42776  irrapxlem2  42779  oasubex  43248  tfsconcatlem  43298  tfsconcatrev  43310  cvgdvgrat  44282  expgrowth  44304  projf1o  45104  ssfiunibd  45224  supxrgere  45248  supxrgelem  45252  suplesup  45254  infrpge  45266  infleinf  45287  supxrunb3  45314  unb2ltle  45330  uzub  45346  cvgcaule  45407  qinioo  45453  qelioo  45464  climinf  45527  mullimc  45537  islptre  45540  limccog  45541  mullimcf  45544  limcrecl  45550  sumnnodd  45551  neglimc  45568  0ellimcdiv  45570  limclner  45572  allbutfifvre  45596  climleltrp  45597  fnlimabslt  45600  climinf2lem  45627  limsuppnflem  45631  limsupvaluz2  45659  supcnvlimsup  45661  limsupgtlem  45698  liminflelimsupuz  45706  liminflimsupclim  45728  limsupub2  45733  xlimpnfxnegmnf  45735  cncfioobd  45818  stoweidlem7  45928  stoweidlem27  45948  stoweidlem39  45960  stoweidlem48  45969  stoweidlem49  45970  stoweidlem60  45981  stoweidlem61  45982  stoweid  45984  dirkercncflem2  46025  fourierdlem20  46048  fourierdlem39  46067  fourierdlem41  46069  fourierdlem48  46075  fourierdlem49  46076  fourierdlem50  46077  fourierdlem64  46091  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem87  46114  fourierdlem103  46130  fourierdlem104  46131  qndenserrnopnlem  46218  sge0ltfirp  46321  sge0gerpmpt  46323  sge0ltfirpmpt2  46347  sge0isum  46348  sge0pnffigtmpt  46361  sge0pnffsumgt  46363  sge0gtfsumgt  46364  sge0uzfsumgt  46365  nnfoctbdjlem  46376  meaiuninclem  46401  meaiuninc3v  46405  omeiunltfirp  46440  carageniuncllem2  46443  hoicvr  46469  volicorescl  46474  hoidmv1le  46515  hoidmvlelem3  46518  hoiqssbllem3  46545  hspmbllem2  46548  iunhoiioolem  46596  vonioo  46603  vonicc  46606  smfaddlem1  46684  smflimlem2  46693  smflimlem3  46694  smfmullem4  46715  fsetsnfo  46968  2reu8i  47028  imasetpreimafvbijlemfo  47279  2pwp1prmfmtno  47464  proththd  47488  sbgoldbwt  47651  sbgoldbst  47652  sbgoldbalt  47655  bgoldbtbndlem4  47682  bgoldbtbnd  47683  grtriprop  47792  ply1mulgsumlem3  48117  ply1mulgsumlem4  48118  islindeps2  48212  isldepslvec2  48214