Theorem reximdva 3169

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  reximddv  3172  reximdvva  3206  reximddv2  3213  wereu2  5674  frpomin  6342  dffo4  7105  nnaordex  8638  frfi  9288  fisupg  9291  marypha1  9429  fiinfg  9494  wemapsolem  9545  unwdomg  9579  rankr1ai  9793  cofsmo  10264  cfcoflem  10267  inar1  10770  nqerf  10925  prlem936  11042  fimaxre  12158  fiminre  12161  arch  12469  bndndx  12471  suprfinzcl  12676  zmin  12928  elpq  12959  qbtwnxr  13179  qsqueeze  13180  qextltlem  13181  xrsupsslem  13286  xrinfmsslem  13287  xrub  13291  supxrunb1  13298  ssnn0fi  13950  fsuppmapnn0fiub0  13958  fsuppmapnn0fz  13961  expnlbnd2  14197  r19.29uz  15297  cau3lem  15301  rlim2lt  15441  rlimclim  15490  2clim  15516  o1co  15530  climcn1  15536  climcn2  15537  rlimo1  15561  climsqz  15585  climsqz2  15586  rlimsqzlem  15595  lo1le  15598  climsup  15616  climcau  15617  caucvgrlem2  15621  iseralt  15631  cvgcmp  15762  cvgcmpce  15764  supcvg  15802  rpnnen2lem12  16168  bezoutlem1  16481  divgcdcoprmex  16603  exprmfct  16641  prmdvdsfz  16642  prmdvdsncoprmbd  16663  pclem  16771  pc2dvds  16812  pcprmpw  16816  dvdsprmpweqle  16819  unbenlem  16841  infpnlem2  16844  infpn2  16846  prmunb  16847  vdwlem2  16915  ramub1lem2  16960  prmdvdsprmop  16976  prmgaplem7  16990  ipodrsima  18494  smndex1mgm  18788  grpinveu  18859  dfgrp3lem  18921  psgneu  19374  odbezout  19426  sylow2blem3  19490  nn0gsumfz  19852  irredrmul  20241  lbsextlem2  20772  znunit  21119  mptcoe1fsupp  21739  scmate  22012  scmatscm  22015  scmatfo  22032  mat1scmat  22041  pmatcoe1fsupp  22203  pmatcollpwfi  22284  pmatcollpw3fi  22287  mptcoe1matfsupp  22304  pm2mp  22327  chmaidscmat  22350  cpmadumatpoly  22385  chcoeffeq  22388  cayhamlem3  22389  cayhamlem4  22390  neiptopnei  22636  neitr  22684  cnpnei  22768  haust1  22856  isnrm3  22863  isreg2  22881  tgcmp  22905  hauscmplem  22910  hauscmp  22911  bwth  22914  1stcfb  22949  1stcelcls  22965  lly1stc  23000  txcmplem1  23145  txlm  23152  xkococnlem  23163  filuni  23389  filufint  23424  ufilen  23434  fclscf  23529  cnextcn  23571  ustex2sym  23721  ustex3sym  23722  utopreg  23757  isucn2  23784  ucnima  23786  ucncn  23790  neipcfilu  23801  metequiv2  24019  metrest  24033  xrsmopn  24328  mulc1cncf  24421  cncfco  24423  bndth  24474  lmmcvg  24778  cfil3i  24786  iscau4  24796  cmetcaulem  24805  iscmet3lem1  24808  caussi  24814  equivcfil  24816  equivcau  24817  caubl  24825  minveclem3b  24945  ovolgelb  24997  ovollb2lem  25005  ovolctb  25007  ovolicc2lem4  25037  ioombl1lem4  25078  dyadmax  25115  volsup2  25122  itg2monolem1  25268  c1liplem1  25513  c1lip1  25514  dvivthlem1  25525  lhop1  25531  ftc1a  25554  ftc1lem6  25558  ply1divex  25654  elply2  25710  dgrlem  25743  aacjcl  25840  aalioulem2  25846  aalioulem3  25847  aalioulem4  25848  ulmcaulem  25906  ulmcau  25907  ulmss  25909  mtest  25916  itgulm  25920  reeff1o  25959  efif1olem4  26054  rlimcnp  26470  xrlimcnp  26473  lgamucov  26542  ftalem3  26579  fta  26584  muval1  26637  dvdssqf  26642  mumullem1  26683  lgsqrmod  26855  lgsqrmodndvds  26856  pntlem3  27112  ostth  27142  nosupno  27206  nosupbnd1lem4  27214  noinfno  27221  noinfbnd1lem4  27229  conway  27300  etasslt  27314  tgtrisegint  27750  tgbtwndiff  27757  tgcgrxfr  27769  lnext  27818  legov2  27837  legtrd  27840  hlcgrex  27867  colperpexlem3  27983  colperpex  27984  hlpasch  28007  hpgerlem  28016  hpgtr  28019  dfcgra2  28081  acopy  28084  inagswap  28092  inaghl  28096  cgrg3col4  28104  axpasch  28199  wwlksnredwwlkn0  29150  midwwlks2s3  29206  clwwlkn1loopb  29296  2pthfrgrrn2  29536  frgrwopreg1  29571  frgrwopreg2  29572  grpoidinvlem3  29759  grpoideu  29762  grpoinveu  29772  ubthlem1  30123  minvecolem5  30134  htthlem  30170  chscllem2  30891  nmopun  31267  lnconi  31286  rnbra  31360  sumdmdii  31668  cdj3lem2b  31690  foresf1o  31742  acunirnmpt  31884  xrofsup  31980  fprodex01  32031  isarchi3  32333  isarchiofld  32435  evls1fpws  32646  lmxrge0  32932  lmdvg  32933  esumlub  33058  esumfsup  33068  esumcvg  33084  ftc2re  33610  cusgr3cyclex  34127  cvmliftmolem2  34273  cvmlift2lem12  34305  satfv1  34354  satffunlem1lem2  34394  satffunlem2lem2  34397  satfv0fvfmla0  34404  wzel  34796  wsuclem  34797  btwndiff  34999  trisegint  35000  cgrxfr  35027  lineext  35048  segcon2  35077  brsegle2  35081  seglecgr12im  35082  segletr  35086  broutsideof3  35098  opnrebl2  35206  nn0prpw  35208  fin2so  36475  poimirlem27  36515  poimirlem30  36518  poimirlem31  36519  poimir  36521  mblfinlem1  36525  mblfinlem2  36526  mblfinlem3  36527  mblfinlem4  36528  itg2addnclem  36539  ftc1cnnc  36560  ftc1anclem5  36565  sdclem1  36611  geomcau  36627  equivtotbnd  36646  bndss  36654  ismtybndlem  36674  heibor1lem  36677  rrncmslem  36700  rngo2  36775  prtlem15  37745  lsateln0  37865  lsat0cv  37903  eqlkr3  37971  lkrshp  37975  lshpset2N  37989  hlhgt2  38260  hlrelat2  38274  atle  38307  athgt  38327  2dim  38341  1cvratex  38344  ps-2  38349  dalem20  38564  lhpexle1lem  38878  lhpexle1  38879  lhpexle2lem  38880  lhpmcvr5N  38898  lhpmcvr6N  38899  cdleme25a  39224  cdleme29ex  39245  cdlemfnid  39435  cdlemg33b0  39572  cdlemg33a  39577  cdlemg35  39584  cdleml3N  39849  dihlsscpre  40105  dih1dimb2  40112  dihatexv  40209  dvh3dim2  40319  dochkr1  40349  dochkr1OLDN  40350  lcfl8  40373  lcfl8b  40375  lcfrlem5  40417  lcfrlem6  40418  mapdrvallem2  40516  mapdh9a  40660  mapdh9aOLDN  40661  hdmaprnlem3eN  40729  hdmaprnlem16N  40733  flt4lem5elem  41393  flt4lem7  41401  nna4b4nsq  41402  fphpdo  41555  rencldnfilem  41558  irrapxlem2  41561  oasubex  42036  tfsconcatlem  42086  tfsconcatrev  42098  cvgdvgrat  43072  expgrowth  43094  projf1o  43896  ssfiunibd  44019  supxrgere  44043  supxrgelem  44047  suplesup  44049  infrpge  44061  infleinf  44082  supxrunb3  44109  unb2ltle  44125  uzub  44141  cvgcaule  44202  qinioo  44248  qelioo  44259  climinf  44322  mullimc  44332  islptre  44335  limccog  44336  mullimcf  44339  limcrecl  44345  sumnnodd  44346  neglimc  44363  0ellimcdiv  44365  limclner  44367  allbutfifvre  44391  climleltrp  44392  fnlimabslt  44395  climinf2lem  44422  limsuppnflem  44426  limsupvaluz2  44454  supcnvlimsup  44456  limsupgtlem  44493  liminflelimsupuz  44501  liminflimsupclim  44523  limsupub2  44528  xlimpnfxnegmnf  44530  cncfioobd  44613  stoweidlem7  44723  stoweidlem27  44743  stoweidlem39  44755  stoweidlem48  44764  stoweidlem49  44765  stoweidlem60  44776  stoweidlem61  44777  stoweid  44779  dirkercncflem2  44820  fourierdlem20  44843  fourierdlem39  44862  fourierdlem41  44864  fourierdlem48  44870  fourierdlem49  44871  fourierdlem50  44872  fourierdlem64  44886  fourierdlem73  44895  fourierdlem74  44896  fourierdlem75  44897  fourierdlem87  44909  fourierdlem103  44925  fourierdlem104  44926  qndenserrnopnlem  45013  sge0ltfirp  45116  sge0gerpmpt  45118  sge0ltfirpmpt2  45142  sge0isum  45143  sge0pnffigtmpt  45156  sge0pnffsumgt  45158  sge0gtfsumgt  45159  sge0uzfsumgt  45160  nnfoctbdjlem  45171  meaiuninclem  45196  meaiuninc3v  45200  omeiunltfirp  45235  carageniuncllem2  45238  hoicvr  45264  volicorescl  45269  hoidmv1le  45310  hoidmvlelem3  45313  hoiqssbllem3  45340  hspmbllem2  45343  iunhoiioolem  45391  vonioo  45398  vonicc  45401  smfaddlem1  45479  smflimlem2  45488  smflimlem3  45489  smfmullem4  45510  fsetsnfo  45763  2reu8i  45821  imasetpreimafvbijlemfo  46073  2pwp1prmfmtno  46258  proththd  46282  sbgoldbwt  46445  sbgoldbst  46446  sbgoldbalt  46449  bgoldbtbndlem4  46476  bgoldbtbnd  46477  zrninitoringc  46969  ply1mulgsumlem3  47069  ply1mulgsumlem4  47070  islindeps2  47164  isldepslvec2  47166