Theorem reximdva 3178

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 417	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	reximdvai 3176	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is referenced by:  reximddv  3181  reximdvva  3213  reximddv2  3224  wereu2  5660  frpomin  6343  dffo4  7100  nnaordex  8625  frfi  9246  fisupg  9249  marypha1  9395  fiinfg  9462  wemapsolem  9513  unwdomg  9547  rankr1ai  9771  cofsmo  10254  cfcoflem  10257  inar1  10761  nqerf  10916  prlem936  11033  fimaxre  12160  fiminre  12163  arch  12502  bndndx  12504  suprfinzcl  12711  zmin  12969  elpq  13000  qbtwnxr  13227  qsqueeze  13228  qextltlem  13229  xrsupsslem  13334  xrinfmsslem  13335  xrub  13339  supxrunb1  13346  ssnn0fi  14023  fsuppmapnn0fiub0  14031  fsuppmapnn0fz  14034  expnlbnd2  14272  r19.29uz  15404  cau3lem  15408  rlim2lt  15550  rlimclim  15599  2clim  15625  o1co  15639  climcn1  15645  climcn2  15646  rlimo1  15670  climsqz  15694  climsqz2  15695  rlimsqzlem  15702  lo1le  15705  climsup  15723  climcau  15724  caucvgrlem2  15728  iseralt  15738  cvgcmp  15870  cvgcmpce  15872  supcvg  15912  rpnnen2lem12  16282  bezoutlem1  16598  divgcdcoprmex  16725  exprmfct  16764  prmdvdsfz  16765  prmdvdsncoprmbd  16787  pclem  16899  pc2dvds  16940  pcprmpw  16944  dvdsprmpweqle  16947  unbenlem  16969  infpnlem2  16972  infpn2  16974  prmunb  16975  vdwlem2  17043  ramub1lem2  17088  prmdvdsprmop  17104  prmgaplem7  17118  ipodrsima  18598  smndex1mgm  18970  grpinveu  19042  dfgrp3lem  19105  psgneu  19577  odbezout  19629  sylow2blem3  19693  nn0gsumfz  20055  irredrmul  20510  zrninitoringc  20762  lbsextlem2  21264  znunit  21694  mptcoe1fsupp  22356  evls1fpws  22510  scmate  22648  scmatscm  22651  scmatfo  22668  mat1scmat  22677  pmatcoe1fsupp  22839  pmatcollpwfi  22920  pmatcollpw3fi  22923  mptcoe1matfsupp  22940  pm2mp  22963  chmaidscmat  22986  cpmadumatpoly  23021  chcoeffeq  23024  cayhamlem3  23025  cayhamlem4  23026  neiptopnei  23270  neitr  23318  cnpnei  23402  haust1  23490  isnrm3  23497  isreg2  23515  tgcmp  23539  hauscmplem  23544  hauscmp  23545  bwth  23548  1stcfb  23583  1stcelcls  23599  lly1stc  23634  txcmplem1  23779  txlm  23786  xkococnlem  23797  filuni  24023  filufint  24058  ufilen  24068  fclscf  24163  cnextcn  24205  ustex2sym  24355  ustex3sym  24356  utopreg  24390  isucn2  24416  ucnima  24418  ucncn  24422  neipcfilu  24433  metequiv2  24648  metrest  24662  xrsmopn  24951  mulc1cncf  25045  cncfco  25047  bndth  25098  lmmcvg  25401  cfil3i  25409  iscau4  25419  cmetcaulem  25428  iscmet3lem1  25431  caussi  25437  equivcfil  25439  equivcau  25440  caubl  25448  minveclem3b  25568  ovolgelb  25620  ovollb2lem  25628  ovolctb  25630  ovolicc2lem4  25660  ioombl1lem4  25701  dyadmax  25738  volsup2  25745  itg2monolem1  25890  c1liplem1  26136  c1lip1  26137  dvivthlem1  26148  lhop1  26154  ftc1a  26177  ftc1lem6  26181  ply1divex  26275  elply2  26334  dgrlem  26367  aacjcl  26471  aalioulem2  26477  aalioulem3  26478  aalioulem4  26479  ulmcaulem  26538  ulmcau  26539  ulmss  26541  mtest  26548  itgulm  26552  reeff1o  26591  efif1olem4  26691  rlimcnp  27111  xrlimcnp  27114  lgamucov  27183  ftalem3  27220  fta  27225  muval1  27278  dvdssqf  27283  mumullem1  27324  lgsqrmod  27497  lgsqrmodndvds  27498  pntlem3  27754  ostth  27784  nosupno  27848  nosupbnd1lem4  27856  noinfno  27863  noinfbnd1lem4  27871  conway  27953  etaslts  27967  znegscl  28566  tgtrisegint  28749  tgbtwndiff  28756  tgcgrxfr  28768  lnext  28817  legov2  28836  legtrd  28839  hlcgrex  28869  colperpexlem3  28994  colperpex  28995  hlpasch  29019  hpgerlem  29028  hpgtr  29031  dfcgra2  29122  acopy  29125  inagswap  29139  inaghl  29143  cgrg3col4  29151  axpasch  29272  wwlksnredwwlkn0  30226  midwwlks2s3  30282  clwwlkn1loopb  30375  2pthfrgrrn2  30615  frgrwopreg1  30650  frgrwopreg2  30651  grpoidinvlem3  30839  grpoideu  30842  grpoinveu  30852  ubthlem1  31203  minvecolem5  31214  htthlem  31250  chscllem2  31971  nmopun  32347  lnconi  32366  rnbra  32440  sumdmdii  32748  cdj3lem2b  32770  foresf1o  32831  acunirnmpt  32985  xrofsup  33093  fprodex01  33150  mndlactfo  33328  mndractfo  33330  isarchi3  33488  isarchiofld  33500  erler  33566  erld2  33567  dfufd2lem  33820  constrconj  34116  constrextdg2lem  34119  constrcjcl  34139  lmxrge0  34323  lmdvg  34324  esumlub  34431  esumfsup  34441  esumcvg  34457  ftc2re  34966  cusgr3cyclex  35609  cvmliftmolem2  35755  cvmlift2lem12  35787  satfv1  35836  satffunlem1lem2  35876  satffunlem2lem2  35879  satfv0fvfmla0  35886  ellcsrspsn  36114  r1peuqusdeg1  36116  wzel  36295  wsuclem  36296  btwndiff  36500  trisegint  36501  cgrxfr  36528  lineext  36549  segcon2  36578  brsegle2  36582  seglecgr12im  36583  segletr  36587  broutsideof3  36599  opnrebl2  36813  nn0prpw  36815  fin2so  38239  poimirlem27  38279  poimirlem30  38282  poimirlem31  38283  poimir  38285  mblfinlem1  38289  mblfinlem2  38290  mblfinlem3  38291  mblfinlem4  38292  itg2addnclem  38303  ftc1cnnc  38324  ftc1anclem5  38329  sdclem1  38375  geomcau  38391  equivtotbnd  38410  bndss  38418  ismtybndlem  38438  heibor1lem  38441  rrncmslem  38464  rngo2  38539  prtlem15  39630  lsateln0  39750  lsat0cv  39788  eqlkr3  39856  lkrshp  39860  lshpset2N  39874  hlhgt2  40144  hlrelat2  40158  atle  40191  athgt  40211  2dim  40225  1cvratex  40228  ps-2  40233  dalem20  40448  lhpexle1lem  40762  lhpexle1  40763  lhpexle2lem  40764  lhpmcvr5N  40782  lhpmcvr6N  40783  cdleme25a  41108  cdleme29ex  41129  cdlemfnid  41319  cdlemg33b0  41456  cdlemg33a  41461  cdlemg35  41468  cdleml3N  41733  dihlsscpre  41989  dih1dimb2  41996  dihatexv  42093  dvh3dim2  42203  dochkr1  42233  dochkr1OLDN  42234  lcfl8  42257  lcfl8b  42259  lcfrlem5  42301  lcfrlem6  42302  mapdrvallem2  42400  mapdh9a  42544  mapdh9aOLDN  42545  hdmaprnlem3eN  42613  hdmaprnlem16N  42617  mndmolinv  42843  primrootsunit1  42845  flt4lem5elem  43366  flt4lem7  43374  nna4b4nsq  43375  fphpdo  43527  rencldnfilem  43530  irrapxlem2  43533  oasubex  43996  tfsconcatlem  44046  tfsconcatrev  44058  cvgdvgrat  45006  expgrowth  45028  projf1o  45897  ssfiunibd  46011  supxrgere  46032  supxrgelem  46036  suplesup  46038  infrpge  46050  infleinf  46070  supxrunb3  46097  unb2ltle  46112  uzub  46128  cvgcaule  46188  qinioo  46234  qelioo  46245  climinf  46305  mullimc  46315  islptre  46318  limccog  46319  mullimcf  46322  limcrecl  46328  sumnnodd  46329  neglimc  46344  0ellimcdiv  46346  limclner  46348  allbutfifvre  46372  climleltrp  46373  fnlimabslt  46376  climinf2lem  46403  limsuppnflem  46407  limsupvaluz2  46435  supcnvlimsup  46437  limsupgtlem  46474  liminflelimsupuz  46482  liminflimsupclim  46504  limsupub2  46509  xlimpnfxnegmnf  46511  cncfioobd  46594  stoweidlem7  46704  stoweidlem27  46724  stoweidlem39  46736  stoweidlem48  46745  stoweidlem49  46746  stoweidlem60  46757  stoweidlem61  46758  stoweid  46760  dirkercncflem2  46801  fourierdlem20  46824  fourierdlem39  46843  fourierdlem41  46845  fourierdlem48  46851  fourierdlem49  46852  fourierdlem50  46853  fourierdlem64  46867  fourierdlem73  46876  fourierdlem74  46877  fourierdlem75  46878  fourierdlem87  46890  fourierdlem103  46906  fourierdlem104  46907  qndenserrnopnlem  46994  sge0ltfirp  47097  sge0gerpmpt  47099  sge0ltfirpmpt2  47123  sge0isum  47124  sge0pnffigtmpt  47137  sge0pnffsumgt  47139  sge0gtfsumgt  47140  sge0uzfsumgt  47141  nnfoctbdjlem  47152  meaiuninclem  47177  meaiuninc3v  47181  omeiunltfirp  47216  carageniuncllem2  47219  volicorescl  47250  hoidmv1le  47291  hoidmvlelem3  47294  hoiqssbllem3  47321  hspmbllem2  47324  iunhoiioolem  47372  vonioo  47379  vonicc  47382  smfaddlem1  47460  smflimlem2  47469  smflimlem3  47470  smfmullem4  47491  fsetsnfo  47773  2reu8i  47833  imasetpreimafvbijlemfo  48137  2pwp1prmfmtno  48325  proththd  48349  sbgoldbwt  48525  sbgoldbst  48526  sbgoldbalt  48529  bgoldbtbndlem4  48556  bgoldbtbnd  48557  grtriprop  48689  ply1mulgsumlem3  49151  ply1mulgsumlem4  49152  islindeps2  49246  isldepslvec2  49248