Theorem reximdva 3149

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3061

This theorem is referenced by:  reximddv  3152  reximdvva  3184  reximddv2  3195  wereu2  5621  frpomin  6298  dffo4  7048  nnaordex  8566  frfi  9185  fisupg  9188  marypha1  9337  fiinfg  9404  wemapsolem  9455  unwdomg  9489  rankr1ai  9710  cofsmo  10179  cfcoflem  10182  inar1  10686  nqerf  10841  prlem936  10958  fimaxre  12086  fiminre  12089  arch  12398  bndndx  12400  suprfinzcl  12606  zmin  12857  elpq  12888  qbtwnxr  13115  qsqueeze  13116  qextltlem  13117  xrsupsslem  13222  xrinfmsslem  13223  xrub  13227  supxrunb1  13234  ssnn0fi  13908  fsuppmapnn0fiub0  13916  fsuppmapnn0fz  13919  expnlbnd2  14157  r19.29uz  15274  cau3lem  15278  rlim2lt  15420  rlimclim  15469  2clim  15495  o1co  15509  climcn1  15515  climcn2  15516  rlimo1  15540  climsqz  15564  climsqz2  15565  rlimsqzlem  15572  lo1le  15575  climsup  15593  climcau  15594  caucvgrlem2  15598  iseralt  15608  cvgcmp  15739  cvgcmpce  15741  supcvg  15779  rpnnen2lem12  16150  bezoutlem1  16466  divgcdcoprmex  16593  exprmfct  16631  prmdvdsfz  16632  prmdvdsncoprmbd  16654  pclem  16766  pc2dvds  16807  pcprmpw  16811  dvdsprmpweqle  16814  unbenlem  16836  infpnlem2  16839  infpn2  16841  prmunb  16842  vdwlem2  16910  ramub1lem2  16955  prmdvdsprmop  16971  prmgaplem7  16985  ipodrsima  18464  smndex1mgm  18832  grpinveu  18904  dfgrp3lem  18968  psgneu  19435  odbezout  19487  sylow2blem3  19551  nn0gsumfz  19913  irredrmul  20363  zrninitoringc  20609  lbsextlem2  21114  znunit  21518  mptcoe1fsupp  22156  evls1fpws  22313  scmate  22454  scmatscm  22457  scmatfo  22474  mat1scmat  22483  pmatcoe1fsupp  22645  pmatcollpwfi  22726  pmatcollpw3fi  22729  mptcoe1matfsupp  22746  pm2mp  22769  chmaidscmat  22792  cpmadumatpoly  22827  chcoeffeq  22830  cayhamlem3  22831  cayhamlem4  22832  neiptopnei  23076  neitr  23124  cnpnei  23208  haust1  23296  isnrm3  23303  isreg2  23321  tgcmp  23345  hauscmplem  23350  hauscmp  23351  bwth  23354  1stcfb  23389  1stcelcls  23405  lly1stc  23440  txcmplem1  23585  txlm  23592  xkococnlem  23603  filuni  23829  filufint  23864  ufilen  23874  fclscf  23969  cnextcn  24011  ustex2sym  24161  ustex3sym  24162  utopreg  24196  isucn2  24222  ucnima  24224  ucncn  24228  neipcfilu  24239  metequiv2  24454  metrest  24468  xrsmopn  24757  mulc1cncf  24854  cncfco  24856  bndth  24913  lmmcvg  25217  cfil3i  25225  iscau4  25235  cmetcaulem  25244  iscmet3lem1  25247  caussi  25253  equivcfil  25255  equivcau  25256  caubl  25264  minveclem3b  25384  ovolgelb  25437  ovollb2lem  25445  ovolctb  25447  ovolicc2lem4  25477  ioombl1lem4  25518  dyadmax  25555  volsup2  25562  itg2monolem1  25707  c1liplem1  25957  c1lip1  25958  dvivthlem1  25969  lhop1  25975  ftc1a  26000  ftc1lem6  26004  ply1divex  26098  elply2  26157  dgrlem  26190  aacjcl  26291  aalioulem2  26297  aalioulem3  26298  aalioulem4  26299  ulmcaulem  26359  ulmcau  26360  ulmss  26362  mtest  26369  itgulm  26373  reeff1o  26413  efif1olem4  26510  rlimcnp  26931  xrlimcnp  26934  lgamucov  27004  ftalem3  27041  fta  27046  muval1  27099  dvdssqf  27104  mumullem1  27145  lgsqrmod  27319  lgsqrmodndvds  27320  pntlem3  27576  ostth  27606  nosupno  27671  nosupbnd1lem4  27679  noinfno  27686  noinfbnd1lem4  27694  conway  27775  etaslts  27789  znegscl  28388  tgtrisegint  28571  tgbtwndiff  28578  tgcgrxfr  28590  lnext  28639  legov2  28658  legtrd  28661  hlcgrex  28688  colperpexlem3  28804  colperpex  28805  hlpasch  28828  hpgerlem  28837  hpgtr  28840  dfcgra2  28902  acopy  28905  inagswap  28913  inaghl  28917  cgrg3col4  28925  axpasch  29014  wwlksnredwwlkn0  29969  midwwlks2s3  30025  clwwlkn1loopb  30118  2pthfrgrrn2  30358  frgrwopreg1  30393  frgrwopreg2  30394  grpoidinvlem3  30581  grpoideu  30584  grpoinveu  30594  ubthlem1  30945  minvecolem5  30956  htthlem  30992  chscllem2  31713  nmopun  32089  lnconi  32108  rnbra  32182  sumdmdii  32490  cdj3lem2b  32512  foresf1o  32579  acunirnmpt  32737  xrofsup  32847  fprodex01  32906  mndlactfo  33109  mndractfo  33111  isarchi3  33269  isarchiofld  33281  erler  33347  dfufd2lem  33630  constrconj  33902  constrextdg2lem  33905  constrcjcl  33925  lmxrge0  34109  lmdvg  34110  esumlub  34217  esumfsup  34227  esumcvg  34243  ftc2re  34755  cusgr3cyclex  35330  cvmliftmolem2  35476  cvmlift2lem12  35508  satfv1  35557  satffunlem1lem2  35597  satffunlem2lem2  35600  satfv0fvfmla0  35607  ellcsrspsn  35835  r1peuqusdeg1  35837  wzel  36016  wsuclem  36017  btwndiff  36221  trisegint  36222  cgrxfr  36249  lineext  36270  segcon2  36299  brsegle2  36303  seglecgr12im  36304  segletr  36308  broutsideof3  36320  opnrebl2  36515  nn0prpw  36517  fin2so  37808  poimirlem27  37848  poimirlem30  37851  poimirlem31  37852  poimir  37854  mblfinlem1  37858  mblfinlem2  37859  mblfinlem3  37860  mblfinlem4  37861  itg2addnclem  37872  ftc1cnnc  37893  ftc1anclem5  37898  sdclem1  37944  geomcau  37960  equivtotbnd  37979  bndss  37987  ismtybndlem  38007  heibor1lem  38010  rrncmslem  38033  rngo2  38108  prtlem15  39135  lsateln0  39255  lsat0cv  39293  eqlkr3  39361  lkrshp  39365  lshpset2N  39379  hlhgt2  39649  hlrelat2  39663  atle  39696  athgt  39716  2dim  39730  1cvratex  39733  ps-2  39738  dalem20  39953  lhpexle1lem  40267  lhpexle1  40268  lhpexle2lem  40269  lhpmcvr5N  40287  lhpmcvr6N  40288  cdleme25a  40613  cdleme29ex  40634  cdlemfnid  40824  cdlemg33b0  40961  cdlemg33a  40966  cdlemg35  40973  cdleml3N  41238  dihlsscpre  41494  dih1dimb2  41501  dihatexv  41598  dvh3dim2  41708  dochkr1  41738  dochkr1OLDN  41739  lcfl8  41762  lcfl8b  41764  lcfrlem5  41806  lcfrlem6  41807  mapdrvallem2  41905  mapdh9a  42049  mapdh9aOLDN  42050  hdmaprnlem3eN  42118  hdmaprnlem16N  42122  mndmolinv  42349  primrootsunit1  42351  flt4lem5elem  42894  flt4lem7  42902  nna4b4nsq  42903  fphpdo  43059  rencldnfilem  43062  irrapxlem2  43065  oasubex  43528  tfsconcatlem  43578  tfsconcatrev  43590  cvgdvgrat  44554  expgrowth  44576  projf1o  45441  ssfiunibd  45557  supxrgere  45578  supxrgelem  45582  suplesup  45584  infrpge  45596  infleinf  45616  supxrunb3  45643  unb2ltle  45659  uzub  45675  cvgcaule  45735  qinioo  45781  qelioo  45792  climinf  45852  mullimc  45862  islptre  45865  limccog  45866  mullimcf  45869  limcrecl  45875  sumnnodd  45876  neglimc  45891  0ellimcdiv  45893  limclner  45895  allbutfifvre  45919  climleltrp  45920  fnlimabslt  45923  climinf2lem  45950  limsuppnflem  45954  limsupvaluz2  45982  supcnvlimsup  45984  limsupgtlem  46021  liminflelimsupuz  46029  liminflimsupclim  46051  limsupub2  46056  xlimpnfxnegmnf  46058  cncfioobd  46141  stoweidlem7  46251  stoweidlem27  46271  stoweidlem39  46283  stoweidlem48  46292  stoweidlem49  46293  stoweidlem60  46304  stoweidlem61  46305  stoweid  46307  dirkercncflem2  46348  fourierdlem20  46371  fourierdlem39  46390  fourierdlem41  46392  fourierdlem48  46398  fourierdlem49  46399  fourierdlem50  46400  fourierdlem64  46414  fourierdlem73  46423  fourierdlem74  46424  fourierdlem75  46425  fourierdlem87  46437  fourierdlem103  46453  fourierdlem104  46454  qndenserrnopnlem  46541  sge0ltfirp  46644  sge0gerpmpt  46646  sge0ltfirpmpt2  46670  sge0isum  46671  sge0pnffigtmpt  46684  sge0pnffsumgt  46686  sge0gtfsumgt  46687  sge0uzfsumgt  46688  nnfoctbdjlem  46699  meaiuninclem  46724  meaiuninc3v  46728  omeiunltfirp  46763  carageniuncllem2  46766  hoicvr  46792  volicorescl  46797  hoidmv1le  46838  hoidmvlelem3  46841  hoiqssbllem3  46868  hspmbllem2  46871  iunhoiioolem  46919  vonioo  46926  vonicc  46929  smfaddlem1  47007  smflimlem2  47016  smflimlem3  47017  smfmullem4  47038  fsetsnfo  47299  2reu8i  47359  imasetpreimafvbijlemfo  47651  2pwp1prmfmtno  47836  proththd  47860  sbgoldbwt  48023  sbgoldbst  48024  sbgoldbalt  48027  bgoldbtbndlem4  48054  bgoldbtbnd  48055  grtriprop  48187  ply1mulgsumlem3  48634  ply1mulgsumlem4  48635  islindeps2  48729  isldepslvec2  48731