Theorem reximdva 3179

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3091

This theorem is used by:  reximddv  3182  reximdvva  3214  reximddv2  3225  wereu2  5653  frpomin  6364  dffo4  7130  nnaordex  8678  frfi  9307  fisupg  9310  marypha1  9456  fiinfg  9523  wemapsolem  9574  unwdomg  9608  rankr1ai  9836  cofsmo  10377  cfcoflem  10380  inar1  10890  nqerf  11045  prlem936  11162  fimaxre  12291  fiminre  12294  arch  12633  bndndx  12635  suprfinzcl  12843  zmin  13101  elpq  13133  qbtwnxr  13360  qsqueeze  13361  qextltlem  13362  xrsupsslem  13467  xrinfmsslem  13468  xrub  13472  supxrunb1  13479  ssnn0fi  14158  fsuppmapnn0fiub0  14166  fsuppmapnn0fz  14169  expnlbnd2  14408  r19.29uz  15550  cau3lem  15554  rlim2lt  15696  rlimclim  15745  2clim  15771  o1co  15785  climcn1  15791  climcn2  15792  rlimo1  15816  climsqz  15840  climsqz2  15841  rlimsqzlem  15848  lo1le  15851  climsup  15869  climcau  15870  caucvgrlem2  15874  iseralt  15884  cvgcmp  16015  cvgcmpce  16017  supcvg  16057  rpnnen2lem12  16425  bezoutlem1  16744  divgcdcoprmex  16873  exprmfct  16912  prmdvdsfz  16913  prmdvdsncoprmbd  16935  pclem  17048  pc2dvds  17089  pcprmpw  17093  dvdsprmpweqle  17096  unbenlem  17118  infpnlem2  17121  infpn2  17123  prmunb  17124  vdwlem2  17192  ramub1lem2  17237  prmdvdsprmop  17253  prmgaplem7  17267  ipodrsima  18747  smndex1mgm  19138  grpinveu  19217  dfgrp3lem  19280  psgneu  19753  odbezout  19805  sylow2blem3  19869  nn0gsumfz  20231  irredrmul  20690  zrninitoringc  20961  lbsextlem2  21470  znunit  21902  mptcoe1fsupp  22566  evls1fpws  22720  scmate  22858  scmatscm  22861  scmatfo  22878  mat1scmat  22887  pmatcoe1fsupp  23052  pmatcollpwfi  23133  pmatcollpw3fi  23136  mptcoe1matfsupp  23153  pm2mp  23176  chmaidscmat  23199  cpmadumatpoly  23234  chcoeffeq  23237  cayhamlem3  23238  cayhamlem4  23239  neiptopnei  23483  neitr  23531  cnpnei  23615  haust1  23703  isnrm3  23710  isreg2  23728  tgcmp  23752  hauscmplem  23757  hauscmp  23758  bwth  23761  1stcfb  23796  1stcelcls  23813  lly1stc  23848  txcmplem1  23993  txlm  24000  xkococnlem  24011  filuni  24237  filufint  24272  ufilen  24282  fclscf  24377  cnextcn  24419  ustex2sym  24569  ustex3sym  24570  utopreg  24604  isucn2  24630  ucnima  24632  ucncn  24636  neipcfilu  24647  metequiv2  24862  metrest  24876  xrsmopn  25165  mulc1cncf  25259  cncfco  25261  bndth  25312  lmmcvg  25615  cfil3i  25623  iscau4  25633  cmetcaulem  25642  iscmet3lem1  25645  caussi  25651  equivcfil  25653  equivcau  25654  caubl  25662  minveclem3b  25782  ovolgelb  25834  ovollb2lem  25842  ovolctb  25844  ovolicc2lem4  25874  ioombl1lem4  25915  dyadmax  25952  volsup2  25959  itg2monolem1  26104  c1liplem1  26349  c1lip1  26350  dvivthlem1  26361  lhop1  26367  ftc1a  26390  ftc1lem6  26394  ply1divex  26488  elply2  26547  dgrlem  26581  aacjcl  26687  aalioulem2  26693  aalioulem3  26694  aalioulem4  26695  ulmcaulem  26754  ulmcau  26755  ulmss  26757  mtest  26764  itgulm  26768  reeff1o  26807  efif1olem4  26906  rlimcnp  27326  xrlimcnp  27329  lgamucov  27398  ftalem3  27435  fta  27440  muval1  27493  dvdssqf  27498  mumullem1  27539  lgsqrmod  27712  lgsqrmodndvds  27713  pntlem3  27969  ostth  27999  flt4lem5elem  28014  flt4lem7  28022  nna4b4nsq  28023  fltoprmlem1  28026  nosupno  28093  nosupbnd1lem4  28101  noinfno  28108  noinfbnd1lem4  28116  conway  28198  etaslts  28212  znegscl  28811  tgtrisegint  28995  tgbtwndiff  29002  tgcgrxfr  29014  lnext  29063  legov2  29082  legtrd  29085  hlcgrex  29115  colperpexlem3  29241  colperpex  29242  hlpasch  29267  hpgerlem  29276  hpgtr  29279  dfcgra2  29371  acopy  29374  inagswap  29393  inaghl  29397  cgrg3col4  29405  axpasch  29552  wwlksnredwwlkn0  30518  midwwlks2s3  30574  clwwlkn1loopb  30667  2pthfrgrrn2  30917  frgrwopreg1  30952  frgrwopreg2  30953  grpoidinvlem3  31141  grpoideu  31144  grpoinveu  31154  ubthlem1  31505  minvecolem5  31516  htthlem  31552  chscllem2  32273  nmopun  32649  lnconi  32668  rnbra  32742  sumdmdii  33050  cdj3lem2b  33072  iscgrag  33085  foresf1o  33175  acunirnmpt  33328  xrofsup  33432  fprodex01  33489  mndlactfo  33664  mndractfo  33666  isarchi3  33824  isarchiofld  33836  erler  33902  erld2  33903  dfufd2lem  34165  constrconj  34460  constrextdg2lem  34463  constrcjcl  34483  lmxrge0  34667  lmdvg  34668  esumlub  34775  esumfsup  34785  esumcvg  34801  ftc2re  35310  dfk12  36025  dfk22  36026  dfk32  36027  cusgr3cyclex  36081  cvmliftmolem2  36227  cvmlift2lem12  36259  satfv1  36308  satffunlem1lem2  36348  satffunlem2lem2  36351  satfv0fvfmla0  36358  ellcsrspsn  36586  r1peuqusdeg1  36588  wzel  36777  wsuclem  36778  btwndiff  36983  trisegint  36984  cgrxfr  37011  lineext  37032  segcon2  37061  brsegle2  37065  seglecgr12im  37066  segletr  37070  broutsideof3  37082  opnrebl2  37300  nn0prpw  37302  fin2so  38735  poimirlem27  38770  poimirlem30  38773  poimirlem31  38774  poimir  38776  mblfinlem1  38780  mblfinlem2  38781  mblfinlem3  38782  mblfinlem4  38783  itg2addnclem  38794  ftc1cnnc  38815  ftc1anclem5  38820  sdclem1  38880  geomcau  38896  equivtotbnd  38915  bndss  38923  ismtybndlem  38943  heibor1lem  38946  rrncmslem  38969  rngo2  39044  prtlem15  40135  lsateln0  40255  lsat0cv  40293  eqlkr3  40361  lkrshp  40365  lshpset2N  40379  hlhgt2  40649  hlrelat2  40663  atle  40696  athgt  40716  2dim  40730  1cvratex  40733  ps-2  40738  dalem20  40953  lhpexle1lem  41267  lhpexle1  41268  lhpexle2lem  41269  lhpmcvr5N  41287  lhpmcvr6N  41288  cdleme25a  41613  cdleme29ex  41634  cdlemfnid  41824  cdlemg33b0  41961  cdlemg33a  41966  cdlemg35  41973  cdleml3N  42238  dihlsscpre  42494  dih1dimb2  42501  dihatexv  42598  dvh3dim2  42708  dochkr1  42738  dochkr1OLDN  42739  lcfl8  42762  lcfl8b  42764  lcfrlem5  42806  lcfrlem6  42807  mapdrvallem2  42905  mapdh9a  43049  mapdh9aOLDN  43050  hdmaprnlem3eN  43118  hdmaprnlem16N  43122  mndmolinv  43348  primrootsunit1  43350  fphpdo  44028  rencldnfilem  44031  irrapxlem2  44034  oasubex  44491  tfsconcatlem  44541  tfsconcatrev  44553  cvgdvgrat  45500  expgrowth  45522  projf1o  46426  ssfiunibd  46540  supxrgere  46560  supxrgelem  46564  suplesup  46566  infrpge  46578  infleinf  46598  supxrunb3  46625  unb2ltle  46640  uzub  46656  cvgcaule  46716  qinioo  46762  qelioo  46773  climinf  46833  mullimc  46843  islptre  46846  limccog  46847  mullimcf  46850  limcrecl  46856  sumnnodd  46857  neglimc  46872  0ellimcdiv  46874  limclner  46876  allbutfifvre  46900  climleltrp  46901  fnlimabslt  46904  climinf2lem  46931  limsuppnflem  46935  limsupvaluz2  46963  supcnvlimsup  46965  limsupgtlem  47002  liminflelimsupuz  47010  liminflimsupclim  47032  limsupub2  47037  xlimpnfxnegmnf  47039  cncfioobd  47122  stoweidlem7  47232  stoweidlem27  47252  stoweidlem39  47264  stoweidlem48  47273  stoweidlem49  47274  stoweidlem60  47285  stoweidlem61  47286  stoweid  47288  dirkercncflem2  47329  fourierdlem20  47352  fourierdlem39  47371  fourierdlem41  47373  fourierdlem48  47379  fourierdlem49  47380  fourierdlem50  47381  fourierdlem64  47395  fourierdlem73  47404  fourierdlem74  47405  fourierdlem75  47406  fourierdlem87  47418  fourierdlem103  47434  fourierdlem104  47435  qndenserrnopnlem  47522  sge0ltfirp  47625  sge0gerpmpt  47627  sge0ltfirpmpt2  47651  sge0isum  47652  sge0pnffigtmpt  47665  sge0pnffsumgt  47667  sge0gtfsumgt  47668  sge0uzfsumgt  47669  nnfoctbdjlem  47680  meaiuninclem  47705  meaiuninc3v  47709  omeiunltfirp  47744  carageniuncllem2  47747  volicorescl  47778  hoidmv1le  47819  hoidmvlelem3  47822  hoiqssbllem3  47849  hspmbllem2  47852  iunhoiioolem  47900  vonioo  47907  vonicc  47910  smfaddlem1  47988  smflimlem2  47997  smflimlem3  47998  smfmullem4  48019  fsetsnfo  48338  2reu8i  48399  imasetpreimafvbijlemfo  48702  2pwp1prmfmtno  48890  proththd  48914  sbgoldbwt  49090  sbgoldbst  49091  sbgoldbalt  49094  bgoldbtbndlem4  49121  bgoldbtbnd  49122  grtriprop  49254  ply1mulgsumlem3  49715  ply1mulgsumlem4  49716  islindeps2  49810  isldepslvec2  49812