Theorem reximdva 3142

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 3140	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3053

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 3054

This theorem is referenced by:  reximddv  3145  reximdvva  3177  reximddv2  3188  wereu2  5620  frpomin  6292  dffo4  7041  nnaordex  8563  frfi  9190  fisupg  9193  marypha1  9343  fiinfg  9410  wemapsolem  9461  unwdomg  9495  rankr1ai  9713  cofsmo  10182  cfcoflem  10185  inar1  10688  nqerf  10843  prlem936  10960  fimaxre  12087  fiminre  12090  arch  12399  bndndx  12401  suprfinzcl  12608  zmin  12863  elpq  12894  qbtwnxr  13120  qsqueeze  13121  qextltlem  13122  xrsupsslem  13227  xrinfmsslem  13228  xrub  13232  supxrunb1  13239  ssnn0fi  13910  fsuppmapnn0fiub0  13918  fsuppmapnn0fz  13921  expnlbnd2  14159  r19.29uz  15276  cau3lem  15280  rlim2lt  15422  rlimclim  15471  2clim  15497  o1co  15511  climcn1  15517  climcn2  15518  rlimo1  15542  climsqz  15566  climsqz2  15567  rlimsqzlem  15574  lo1le  15577  climsup  15595  climcau  15596  caucvgrlem2  15600  iseralt  15610  cvgcmp  15741  cvgcmpce  15743  supcvg  15781  rpnnen2lem12  16152  bezoutlem1  16468  divgcdcoprmex  16595  exprmfct  16633  prmdvdsfz  16634  prmdvdsncoprmbd  16656  pclem  16768  pc2dvds  16809  pcprmpw  16813  dvdsprmpweqle  16816  unbenlem  16838  infpnlem2  16841  infpn2  16843  prmunb  16844  vdwlem2  16912  ramub1lem2  16957  prmdvdsprmop  16973  prmgaplem7  16987  ipodrsima  18465  smndex1mgm  18799  grpinveu  18871  dfgrp3lem  18935  psgneu  19403  odbezout  19455  sylow2blem3  19519  nn0gsumfz  19881  irredrmul  20330  zrninitoringc  20579  lbsextlem2  21084  znunit  21488  mptcoe1fsupp  22116  evls1fpws  22272  scmate  22413  scmatscm  22416  scmatfo  22433  mat1scmat  22442  pmatcoe1fsupp  22604  pmatcollpwfi  22685  pmatcollpw3fi  22688  mptcoe1matfsupp  22705  pm2mp  22728  chmaidscmat  22751  cpmadumatpoly  22786  chcoeffeq  22789  cayhamlem3  22790  cayhamlem4  22791  neiptopnei  23035  neitr  23083  cnpnei  23167  haust1  23255  isnrm3  23262  isreg2  23280  tgcmp  23304  hauscmplem  23309  hauscmp  23310  bwth  23313  1stcfb  23348  1stcelcls  23364  lly1stc  23399  txcmplem1  23544  txlm  23551  xkococnlem  23562  filuni  23788  filufint  23823  ufilen  23833  fclscf  23928  cnextcn  23970  ustex2sym  24120  ustex3sym  24121  utopreg  24156  isucn2  24182  ucnima  24184  ucncn  24188  neipcfilu  24199  metequiv2  24414  metrest  24428  xrsmopn  24717  mulc1cncf  24814  cncfco  24816  bndth  24873  lmmcvg  25177  cfil3i  25185  iscau4  25195  cmetcaulem  25204  iscmet3lem1  25207  caussi  25213  equivcfil  25215  equivcau  25216  caubl  25224  minveclem3b  25344  ovolgelb  25397  ovollb2lem  25405  ovolctb  25407  ovolicc2lem4  25437  ioombl1lem4  25478  dyadmax  25515  volsup2  25522  itg2monolem1  25667  c1liplem1  25917  c1lip1  25918  dvivthlem1  25929  lhop1  25935  ftc1a  25960  ftc1lem6  25964  ply1divex  26058  elply2  26117  dgrlem  26150  aacjcl  26251  aalioulem2  26257  aalioulem3  26258  aalioulem4  26259  ulmcaulem  26319  ulmcau  26320  ulmss  26322  mtest  26329  itgulm  26333  reeff1o  26373  efif1olem4  26470  rlimcnp  26891  xrlimcnp  26894  lgamucov  26964  ftalem3  27001  fta  27006  muval1  27059  dvdssqf  27064  mumullem1  27105  lgsqrmod  27279  lgsqrmodndvds  27280  pntlem3  27536  ostth  27566  nosupno  27631  nosupbnd1lem4  27639  noinfno  27646  noinfbnd1lem4  27654  conway  27728  etasslt  27742  znegscl  28303  tgtrisegint  28462  tgbtwndiff  28469  tgcgrxfr  28481  lnext  28530  legov2  28549  legtrd  28552  hlcgrex  28579  colperpexlem3  28695  colperpex  28696  hlpasch  28719  hpgerlem  28728  hpgtr  28731  dfcgra2  28793  acopy  28796  inagswap  28804  inaghl  28808  cgrg3col4  28816  axpasch  28904  wwlksnredwwlkn0  29859  midwwlks2s3  29915  clwwlkn1loopb  30005  2pthfrgrrn2  30245  frgrwopreg1  30280  frgrwopreg2  30281  grpoidinvlem3  30468  grpoideu  30471  grpoinveu  30481  ubthlem1  30832  minvecolem5  30843  htthlem  30879  chscllem2  31600  nmopun  31976  lnconi  31995  rnbra  32069  sumdmdii  32377  cdj3lem2b  32399  foresf1o  32466  acunirnmpt  32616  xrofsup  32723  fprodex01  32783  mndlactfo  32994  mndractfo  32996  isarchi3  33142  isarchiofld  33154  erler  33218  dfufd2lem  33499  constrconj  33714  constrextdg2lem  33717  constrcjcl  33737  lmxrge0  33921  lmdvg  33922  esumlub  34029  esumfsup  34039  esumcvg  34055  ftc2re  34568  cusgr3cyclex  35111  cvmliftmolem2  35257  cvmlift2lem12  35289  satfv1  35338  satffunlem1lem2  35378  satffunlem2lem2  35381  satfv0fvfmla0  35388  ellcsrspsn  35616  r1peuqusdeg1  35618  wzel  35800  wsuclem  35801  btwndiff  36003  trisegint  36004  cgrxfr  36031  lineext  36052  segcon2  36081  brsegle2  36085  seglecgr12im  36086  segletr  36090  broutsideof3  36102  opnrebl2  36297  nn0prpw  36299  fin2so  37589  poimirlem27  37629  poimirlem30  37632  poimirlem31  37633  poimir  37635  mblfinlem1  37639  mblfinlem2  37640  mblfinlem3  37641  mblfinlem4  37642  itg2addnclem  37653  ftc1cnnc  37674  ftc1anclem5  37679  sdclem1  37725  geomcau  37741  equivtotbnd  37760  bndss  37768  ismtybndlem  37788  heibor1lem  37791  rrncmslem  37814  rngo2  37889  prtlem15  38856  lsateln0  38976  lsat0cv  39014  eqlkr3  39082  lkrshp  39086  lshpset2N  39100  hlhgt2  39371  hlrelat2  39385  atle  39418  athgt  39438  2dim  39452  1cvratex  39455  ps-2  39460  dalem20  39675  lhpexle1lem  39989  lhpexle1  39990  lhpexle2lem  39991  lhpmcvr5N  40009  lhpmcvr6N  40010  cdleme25a  40335  cdleme29ex  40356  cdlemfnid  40546  cdlemg33b0  40683  cdlemg33a  40688  cdlemg35  40695  cdleml3N  40960  dihlsscpre  41216  dih1dimb2  41223  dihatexv  41320  dvh3dim2  41430  dochkr1  41460  dochkr1OLDN  41461  lcfl8  41484  lcfl8b  41486  lcfrlem5  41528  lcfrlem6  41529  mapdrvallem2  41627  mapdh9a  41771  mapdh9aOLDN  41772  hdmaprnlem3eN  41840  hdmaprnlem16N  41844  mndmolinv  42071  primrootsunit1  42073  flt4lem5elem  42627  flt4lem7  42635  nna4b4nsq  42636  fphpdo  42793  rencldnfilem  42796  irrapxlem2  42799  oasubex  43262  tfsconcatlem  43312  tfsconcatrev  43324  cvgdvgrat  44289  expgrowth  44311  projf1o  45178  ssfiunibd  45294  supxrgere  45316  supxrgelem  45320  suplesup  45322  infrpge  45334  infleinf  45355  supxrunb3  45382  unb2ltle  45398  uzub  45414  cvgcaule  45474  qinioo  45520  qelioo  45531  climinf  45591  mullimc  45601  islptre  45604  limccog  45605  mullimcf  45608  limcrecl  45614  sumnnodd  45615  neglimc  45632  0ellimcdiv  45634  limclner  45636  allbutfifvre  45660  climleltrp  45661  fnlimabslt  45664  climinf2lem  45691  limsuppnflem  45695  limsupvaluz2  45723  supcnvlimsup  45725  limsupgtlem  45762  liminflelimsupuz  45770  liminflimsupclim  45792  limsupub2  45797  xlimpnfxnegmnf  45799  cncfioobd  45882  stoweidlem7  45992  stoweidlem27  46012  stoweidlem39  46024  stoweidlem48  46033  stoweidlem49  46034  stoweidlem60  46045  stoweidlem61  46046  stoweid  46048  dirkercncflem2  46089  fourierdlem20  46112  fourierdlem39  46131  fourierdlem41  46133  fourierdlem48  46139  fourierdlem49  46140  fourierdlem50  46141  fourierdlem64  46155  fourierdlem73  46164  fourierdlem74  46165  fourierdlem75  46166  fourierdlem87  46178  fourierdlem103  46194  fourierdlem104  46195  qndenserrnopnlem  46282  sge0ltfirp  46385  sge0gerpmpt  46387  sge0ltfirpmpt2  46411  sge0isum  46412  sge0pnffigtmpt  46425  sge0pnffsumgt  46427  sge0gtfsumgt  46428  sge0uzfsumgt  46429  nnfoctbdjlem  46440  meaiuninclem  46465  meaiuninc3v  46469  omeiunltfirp  46504  carageniuncllem2  46507  hoicvr  46533  volicorescl  46538  hoidmv1le  46579  hoidmvlelem3  46582  hoiqssbllem3  46609  hspmbllem2  46612  iunhoiioolem  46660  vonioo  46667  vonicc  46670  smfaddlem1  46748  smflimlem2  46757  smflimlem3  46758  smfmullem4  46779  fsetsnfo  47041  2reu8i  47101  imasetpreimafvbijlemfo  47393  2pwp1prmfmtno  47578  proththd  47602  sbgoldbwt  47765  sbgoldbst  47766  sbgoldbalt  47769  bgoldbtbndlem4  47796  bgoldbtbnd  47797  grtriprop  47929  ply1mulgsumlem3  48377  ply1mulgsumlem4  48378  islindeps2  48472  isldepslvec2  48474