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  5621  frpomin  6298  dffo4  7049  nnaordex  8567  frfi  9188  fisupg  9191  marypha1  9340  fiinfg  9407  wemapsolem  9458  unwdomg  9492  rankr1ai  9713  cofsmo  10182  cfcoflem  10185  inar1  10689  nqerf  10844  prlem936  10961  fimaxre  12091  fiminre  12094  arch  12425  bndndx  12427  suprfinzcl  12634  zmin  12885  elpq  12916  qbtwnxr  13143  qsqueeze  13144  qextltlem  13145  xrsupsslem  13250  xrinfmsslem  13251  xrub  13255  supxrunb1  13262  ssnn0fi  13938  fsuppmapnn0fiub0  13946  fsuppmapnn0fz  13949  expnlbnd2  14187  r19.29uz  15304  cau3lem  15308  rlim2lt  15450  rlimclim  15499  2clim  15525  o1co  15539  climcn1  15545  climcn2  15546  rlimo1  15570  climsqz  15594  climsqz2  15595  rlimsqzlem  15602  lo1le  15605  climsup  15623  climcau  15624  caucvgrlem2  15628  iseralt  15638  cvgcmp  15770  cvgcmpce  15772  supcvg  15812  rpnnen2lem12  16183  bezoutlem1  16499  divgcdcoprmex  16626  exprmfct  16665  prmdvdsfz  16666  prmdvdsncoprmbd  16688  pclem  16800  pc2dvds  16841  pcprmpw  16845  dvdsprmpweqle  16848  unbenlem  16870  infpnlem2  16873  infpn2  16875  prmunb  16876  vdwlem2  16944  ramub1lem2  16989  prmdvdsprmop  17005  prmgaplem7  17019  ipodrsima  18498  smndex1mgm  18869  grpinveu  18941  dfgrp3lem  19005  psgneu  19472  odbezout  19524  sylow2blem3  19588  nn0gsumfz  19950  irredrmul  20398  zrninitoringc  20644  lbsextlem2  21149  znunit  21553  mptcoe1fsupp  22189  evls1fpws  22344  scmate  22485  scmatscm  22488  scmatfo  22505  mat1scmat  22514  pmatcoe1fsupp  22676  pmatcollpwfi  22757  pmatcollpw3fi  22760  mptcoe1matfsupp  22777  pm2mp  22800  chmaidscmat  22823  cpmadumatpoly  22858  chcoeffeq  22861  cayhamlem3  22862  cayhamlem4  22863  neiptopnei  23107  neitr  23155  cnpnei  23239  haust1  23327  isnrm3  23334  isreg2  23352  tgcmp  23376  hauscmplem  23381  hauscmp  23382  bwth  23385  1stcfb  23420  1stcelcls  23436  lly1stc  23471  txcmplem1  23616  txlm  23623  xkococnlem  23634  filuni  23860  filufint  23895  ufilen  23905  fclscf  24000  cnextcn  24042  ustex2sym  24192  ustex3sym  24193  utopreg  24227  isucn2  24253  ucnima  24255  ucncn  24259  neipcfilu  24270  metequiv2  24485  metrest  24499  xrsmopn  24788  mulc1cncf  24882  cncfco  24884  bndth  24935  lmmcvg  25238  cfil3i  25246  iscau4  25256  cmetcaulem  25265  iscmet3lem1  25268  caussi  25274  equivcfil  25276  equivcau  25277  caubl  25285  minveclem3b  25405  ovolgelb  25457  ovollb2lem  25465  ovolctb  25467  ovolicc2lem4  25497  ioombl1lem4  25538  dyadmax  25575  volsup2  25582  itg2monolem1  25727  c1liplem1  25973  c1lip1  25974  dvivthlem1  25985  lhop1  25991  ftc1a  26014  ftc1lem6  26018  ply1divex  26112  elply2  26171  dgrlem  26204  aacjcl  26304  aalioulem2  26310  aalioulem3  26311  aalioulem4  26312  ulmcaulem  26372  ulmcau  26373  ulmss  26375  mtest  26382  itgulm  26386  reeff1o  26425  efif1olem4  26522  rlimcnp  26942  xrlimcnp  26945  lgamucov  27015  ftalem3  27052  fta  27057  muval1  27110  dvdssqf  27115  mumullem1  27156  lgsqrmod  27329  lgsqrmodndvds  27330  pntlem3  27586  ostth  27616  nosupno  27681  nosupbnd1lem4  27689  noinfno  27696  noinfbnd1lem4  27704  conway  27785  etaslts  27799  znegscl  28398  tgtrisegint  28581  tgbtwndiff  28588  tgcgrxfr  28600  lnext  28649  legov2  28668  legtrd  28671  hlcgrex  28698  colperpexlem3  28814  colperpex  28815  hlpasch  28838  hpgerlem  28847  hpgtr  28850  dfcgra2  28912  acopy  28915  inagswap  28923  inaghl  28927  cgrg3col4  28935  axpasch  29024  wwlksnredwwlkn0  29979  midwwlks2s3  30035  clwwlkn1loopb  30128  2pthfrgrrn2  30368  frgrwopreg1  30403  frgrwopreg2  30404  grpoidinvlem3  30592  grpoideu  30595  grpoinveu  30605  ubthlem1  30956  minvecolem5  30967  htthlem  31003  chscllem2  31724  nmopun  32100  lnconi  32119  rnbra  32193  sumdmdii  32501  cdj3lem2b  32523  foresf1o  32589  acunirnmpt  32747  xrofsup  32855  fprodex01  32913  mndlactfo  33102  mndractfo  33104  isarchi3  33263  isarchiofld  33275  erler  33341  dfufd2lem  33624  constrconj  33905  constrextdg2lem  33908  constrcjcl  33928  lmxrge0  34112  lmdvg  34113  esumlub  34220  esumfsup  34230  esumcvg  34246  ftc2re  34758  cusgr3cyclex  35334  cvmliftmolem2  35480  cvmlift2lem12  35512  satfv1  35561  satffunlem1lem2  35601  satffunlem2lem2  35604  satfv0fvfmla0  35611  ellcsrspsn  35839  r1peuqusdeg1  35841  wzel  36020  wsuclem  36021  btwndiff  36225  trisegint  36226  cgrxfr  36253  lineext  36274  segcon2  36303  brsegle2  36307  seglecgr12im  36308  segletr  36312  broutsideof3  36324  opnrebl2  36519  nn0prpw  36521  fin2so  37942  poimirlem27  37982  poimirlem30  37985  poimirlem31  37986  poimir  37988  mblfinlem1  37992  mblfinlem2  37993  mblfinlem3  37994  mblfinlem4  37995  itg2addnclem  38006  ftc1cnnc  38027  ftc1anclem5  38032  sdclem1  38078  geomcau  38094  equivtotbnd  38113  bndss  38121  ismtybndlem  38141  heibor1lem  38144  rrncmslem  38167  rngo2  38242  prtlem15  39335  lsateln0  39455  lsat0cv  39493  eqlkr3  39561  lkrshp  39565  lshpset2N  39579  hlhgt2  39849  hlrelat2  39863  atle  39896  athgt  39916  2dim  39930  1cvratex  39933  ps-2  39938  dalem20  40153  lhpexle1lem  40467  lhpexle1  40468  lhpexle2lem  40469  lhpmcvr5N  40487  lhpmcvr6N  40488  cdleme25a  40813  cdleme29ex  40834  cdlemfnid  41024  cdlemg33b0  41161  cdlemg33a  41166  cdlemg35  41173  cdleml3N  41438  dihlsscpre  41694  dih1dimb2  41701  dihatexv  41798  dvh3dim2  41908  dochkr1  41938  dochkr1OLDN  41939  lcfl8  41962  lcfl8b  41964  lcfrlem5  42006  lcfrlem6  42007  mapdrvallem2  42105  mapdh9a  42249  mapdh9aOLDN  42250  hdmaprnlem3eN  42318  hdmaprnlem16N  42322  mndmolinv  42548  primrootsunit1  42550  flt4lem5elem  43098  flt4lem7  43106  nna4b4nsq  43107  fphpdo  43263  rencldnfilem  43266  irrapxlem2  43269  oasubex  43732  tfsconcatlem  43782  tfsconcatrev  43794  cvgdvgrat  44758  expgrowth  44780  projf1o  45644  ssfiunibd  45760  supxrgere  45781  supxrgelem  45785  suplesup  45787  infrpge  45799  infleinf  45819  supxrunb3  45846  unb2ltle  45861  uzub  45877  cvgcaule  45937  qinioo  45983  qelioo  45994  climinf  46054  mullimc  46064  islptre  46067  limccog  46068  mullimcf  46071  limcrecl  46077  sumnnodd  46078  neglimc  46093  0ellimcdiv  46095  limclner  46097  allbutfifvre  46121  climleltrp  46122  fnlimabslt  46125  climinf2lem  46152  limsuppnflem  46156  limsupvaluz2  46184  supcnvlimsup  46186  limsupgtlem  46223  liminflelimsupuz  46231  liminflimsupclim  46253  limsupub2  46258  xlimpnfxnegmnf  46260  cncfioobd  46343  stoweidlem7  46453  stoweidlem27  46473  stoweidlem39  46485  stoweidlem48  46494  stoweidlem49  46495  stoweidlem60  46506  stoweidlem61  46507  stoweid  46509  dirkercncflem2  46550  fourierdlem20  46573  fourierdlem39  46592  fourierdlem41  46594  fourierdlem48  46600  fourierdlem49  46601  fourierdlem50  46602  fourierdlem64  46616  fourierdlem73  46625  fourierdlem74  46626  fourierdlem75  46627  fourierdlem87  46639  fourierdlem103  46655  fourierdlem104  46656  qndenserrnopnlem  46743  sge0ltfirp  46846  sge0gerpmpt  46848  sge0ltfirpmpt2  46872  sge0isum  46873  sge0pnffigtmpt  46886  sge0pnffsumgt  46888  sge0gtfsumgt  46889  sge0uzfsumgt  46890  nnfoctbdjlem  46901  meaiuninclem  46926  meaiuninc3v  46930  omeiunltfirp  46965  carageniuncllem2  46968  volicorescl  46999  hoidmv1le  47040  hoidmvlelem3  47043  hoiqssbllem3  47070  hspmbllem2  47073  iunhoiioolem  47121  vonioo  47128  vonicc  47131  smfaddlem1  47209  smflimlem2  47218  smflimlem3  47219  smfmullem4  47240  fsetsnfo  47513  2reu8i  47573  imasetpreimafvbijlemfo  47877  2pwp1prmfmtno  48065  proththd  48089  sbgoldbwt  48265  sbgoldbst  48266  sbgoldbalt  48269  bgoldbtbndlem4  48296  bgoldbtbnd  48297  grtriprop  48429  ply1mulgsumlem3  48876  ply1mulgsumlem4  48877  islindeps2  48971  isldepslvec2  48973