Theorem reximdva 3151

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  reximddv  3154  reximdvva  3186  reximddv2  3197  wereu2  5629  frpomin  6306  dffo4  7057  nnaordex  8576  frfi  9197  fisupg  9200  marypha1  9349  fiinfg  9416  wemapsolem  9467  unwdomg  9501  rankr1ai  9722  cofsmo  10191  cfcoflem  10194  inar1  10698  nqerf  10853  prlem936  10970  fimaxre  12098  fiminre  12101  arch  12410  bndndx  12412  suprfinzcl  12618  zmin  12869  elpq  12900  qbtwnxr  13127  qsqueeze  13128  qextltlem  13129  xrsupsslem  13234  xrinfmsslem  13235  xrub  13239  supxrunb1  13246  ssnn0fi  13920  fsuppmapnn0fiub0  13928  fsuppmapnn0fz  13931  expnlbnd2  14169  r19.29uz  15286  cau3lem  15290  rlim2lt  15432  rlimclim  15481  2clim  15507  o1co  15521  climcn1  15527  climcn2  15528  rlimo1  15552  climsqz  15576  climsqz2  15577  rlimsqzlem  15584  lo1le  15587  climsup  15605  climcau  15606  caucvgrlem2  15610  iseralt  15620  cvgcmp  15751  cvgcmpce  15753  supcvg  15791  rpnnen2lem12  16162  bezoutlem1  16478  divgcdcoprmex  16605  exprmfct  16643  prmdvdsfz  16644  prmdvdsncoprmbd  16666  pclem  16778  pc2dvds  16819  pcprmpw  16823  dvdsprmpweqle  16826  unbenlem  16848  infpnlem2  16851  infpn2  16853  prmunb  16854  vdwlem2  16922  ramub1lem2  16967  prmdvdsprmop  16983  prmgaplem7  16997  ipodrsima  18476  smndex1mgm  18844  grpinveu  18916  dfgrp3lem  18980  psgneu  19447  odbezout  19499  sylow2blem3  19563  nn0gsumfz  19925  irredrmul  20375  zrninitoringc  20621  lbsextlem2  21126  znunit  21530  mptcoe1fsupp  22168  evls1fpws  22325  scmate  22466  scmatscm  22469  scmatfo  22486  mat1scmat  22495  pmatcoe1fsupp  22657  pmatcollpwfi  22738  pmatcollpw3fi  22741  mptcoe1matfsupp  22758  pm2mp  22781  chmaidscmat  22804  cpmadumatpoly  22839  chcoeffeq  22842  cayhamlem3  22843  cayhamlem4  22844  neiptopnei  23088  neitr  23136  cnpnei  23220  haust1  23308  isnrm3  23315  isreg2  23333  tgcmp  23357  hauscmplem  23362  hauscmp  23363  bwth  23366  1stcfb  23401  1stcelcls  23417  lly1stc  23452  txcmplem1  23597  txlm  23604  xkococnlem  23615  filuni  23841  filufint  23876  ufilen  23886  fclscf  23981  cnextcn  24023  ustex2sym  24173  ustex3sym  24174  utopreg  24208  isucn2  24234  ucnima  24236  ucncn  24240  neipcfilu  24251  metequiv2  24466  metrest  24480  xrsmopn  24769  mulc1cncf  24866  cncfco  24868  bndth  24925  lmmcvg  25229  cfil3i  25237  iscau4  25247  cmetcaulem  25256  iscmet3lem1  25259  caussi  25265  equivcfil  25267  equivcau  25268  caubl  25276  minveclem3b  25396  ovolgelb  25449  ovollb2lem  25457  ovolctb  25459  ovolicc2lem4  25489  ioombl1lem4  25530  dyadmax  25567  volsup2  25574  itg2monolem1  25719  c1liplem1  25969  c1lip1  25970  dvivthlem1  25981  lhop1  25987  ftc1a  26012  ftc1lem6  26016  ply1divex  26110  elply2  26169  dgrlem  26202  aacjcl  26303  aalioulem2  26309  aalioulem3  26310  aalioulem4  26311  ulmcaulem  26371  ulmcau  26372  ulmss  26374  mtest  26381  itgulm  26385  reeff1o  26425  efif1olem4  26522  rlimcnp  26943  xrlimcnp  26946  lgamucov  27016  ftalem3  27053  fta  27058  muval1  27111  dvdssqf  27116  mumullem1  27157  lgsqrmod  27331  lgsqrmodndvds  27332  pntlem3  27588  ostth  27618  nosupno  27683  nosupbnd1lem4  27691  noinfno  27698  noinfbnd1lem4  27706  conway  27787  etaslts  27801  znegscl  28400  tgtrisegint  28583  tgbtwndiff  28590  tgcgrxfr  28602  lnext  28651  legov2  28670  legtrd  28673  hlcgrex  28700  colperpexlem3  28816  colperpex  28817  hlpasch  28840  hpgerlem  28849  hpgtr  28852  dfcgra2  28914  acopy  28917  inagswap  28925  inaghl  28929  cgrg3col4  28937  axpasch  29026  wwlksnredwwlkn0  29981  midwwlks2s3  30037  clwwlkn1loopb  30130  2pthfrgrrn2  30370  frgrwopreg1  30405  frgrwopreg2  30406  grpoidinvlem3  30593  grpoideu  30596  grpoinveu  30606  ubthlem1  30957  minvecolem5  30968  htthlem  31004  chscllem2  31725  nmopun  32101  lnconi  32120  rnbra  32194  sumdmdii  32502  cdj3lem2b  32524  foresf1o  32590  acunirnmpt  32748  xrofsup  32857  fprodex01  32916  mndlactfo  33119  mndractfo  33121  isarchi3  33280  isarchiofld  33292  erler  33358  dfufd2lem  33641  constrconj  33922  constrextdg2lem  33925  constrcjcl  33945  lmxrge0  34129  lmdvg  34130  esumlub  34237  esumfsup  34247  esumcvg  34263  ftc2re  34775  cusgr3cyclex  35349  cvmliftmolem2  35495  cvmlift2lem12  35527  satfv1  35576  satffunlem1lem2  35616  satffunlem2lem2  35619  satfv0fvfmla0  35626  ellcsrspsn  35854  r1peuqusdeg1  35856  wzel  36035  wsuclem  36036  btwndiff  36240  trisegint  36241  cgrxfr  36268  lineext  36289  segcon2  36318  brsegle2  36322  seglecgr12im  36323  segletr  36327  broutsideof3  36339  opnrebl2  36534  nn0prpw  36536  fin2so  37855  poimirlem27  37895  poimirlem30  37898  poimirlem31  37899  poimir  37901  mblfinlem1  37905  mblfinlem2  37906  mblfinlem3  37907  mblfinlem4  37908  itg2addnclem  37919  ftc1cnnc  37940  ftc1anclem5  37945  sdclem1  37991  geomcau  38007  equivtotbnd  38026  bndss  38034  ismtybndlem  38054  heibor1lem  38057  rrncmslem  38080  rngo2  38155  prtlem15  39248  lsateln0  39368  lsat0cv  39406  eqlkr3  39474  lkrshp  39478  lshpset2N  39492  hlhgt2  39762  hlrelat2  39776  atle  39809  athgt  39829  2dim  39843  1cvratex  39846  ps-2  39851  dalem20  40066  lhpexle1lem  40380  lhpexle1  40381  lhpexle2lem  40382  lhpmcvr5N  40400  lhpmcvr6N  40401  cdleme25a  40726  cdleme29ex  40747  cdlemfnid  40937  cdlemg33b0  41074  cdlemg33a  41079  cdlemg35  41086  cdleml3N  41351  dihlsscpre  41607  dih1dimb2  41614  dihatexv  41711  dvh3dim2  41821  dochkr1  41851  dochkr1OLDN  41852  lcfl8  41875  lcfl8b  41877  lcfrlem5  41919  lcfrlem6  41920  mapdrvallem2  42018  mapdh9a  42162  mapdh9aOLDN  42163  hdmaprnlem3eN  42231  hdmaprnlem16N  42235  mndmolinv  42462  primrootsunit1  42464  flt4lem5elem  43006  flt4lem7  43014  nna4b4nsq  43015  fphpdo  43171  rencldnfilem  43174  irrapxlem2  43177  oasubex  43640  tfsconcatlem  43690  tfsconcatrev  43702  cvgdvgrat  44666  expgrowth  44688  projf1o  45552  ssfiunibd  45668  supxrgere  45689  supxrgelem  45693  suplesup  45695  infrpge  45707  infleinf  45727  supxrunb3  45754  unb2ltle  45770  uzub  45786  cvgcaule  45846  qinioo  45892  qelioo  45903  climinf  45963  mullimc  45973  islptre  45976  limccog  45977  mullimcf  45980  limcrecl  45986  sumnnodd  45987  neglimc  46002  0ellimcdiv  46004  limclner  46006  allbutfifvre  46030  climleltrp  46031  fnlimabslt  46034  climinf2lem  46061  limsuppnflem  46065  limsupvaluz2  46093  supcnvlimsup  46095  limsupgtlem  46132  liminflelimsupuz  46140  liminflimsupclim  46162  limsupub2  46167  xlimpnfxnegmnf  46169  cncfioobd  46252  stoweidlem7  46362  stoweidlem27  46382  stoweidlem39  46394  stoweidlem48  46403  stoweidlem49  46404  stoweidlem60  46415  stoweidlem61  46416  stoweid  46418  dirkercncflem2  46459  fourierdlem20  46482  fourierdlem39  46501  fourierdlem41  46503  fourierdlem48  46509  fourierdlem49  46510  fourierdlem50  46511  fourierdlem64  46525  fourierdlem73  46534  fourierdlem74  46535  fourierdlem75  46536  fourierdlem87  46548  fourierdlem103  46564  fourierdlem104  46565  qndenserrnopnlem  46652  sge0ltfirp  46755  sge0gerpmpt  46757  sge0ltfirpmpt2  46781  sge0isum  46782  sge0pnffigtmpt  46795  sge0pnffsumgt  46797  sge0gtfsumgt  46798  sge0uzfsumgt  46799  nnfoctbdjlem  46810  meaiuninclem  46835  meaiuninc3v  46839  omeiunltfirp  46874  carageniuncllem2  46877  hoicvr  46903  volicorescl  46908  hoidmv1le  46949  hoidmvlelem3  46952  hoiqssbllem3  46979  hspmbllem2  46982  iunhoiioolem  47030  vonioo  47037  vonicc  47040  smfaddlem1  47118  smflimlem2  47127  smflimlem3  47128  smfmullem4  47149  fsetsnfo  47410  2reu8i  47470  imasetpreimafvbijlemfo  47762  2pwp1prmfmtno  47947  proththd  47971  sbgoldbwt  48134  sbgoldbst  48135  sbgoldbalt  48138  bgoldbtbndlem4  48165  bgoldbtbnd  48166  grtriprop  48298  ply1mulgsumlem3  48745  ply1mulgsumlem4  48746  islindeps2  48840  isldepslvec2  48842