Theorem reximdva 3155

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2107  ∃wrex 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-rex 3060

This theorem is referenced by:  reximddv  3158  reximdvva  3194  reximddv2  3202  wereu2  5662  frpomin  6340  dffo4  7103  nnaordex  8658  frfi  9303  fisupg  9306  marypha1  9456  fiinfg  9521  wemapsolem  9572  unwdomg  9606  rankr1ai  9820  cofsmo  10291  cfcoflem  10294  inar1  10797  nqerf  10952  prlem936  11069  fimaxre  12194  fiminre  12197  arch  12506  bndndx  12508  suprfinzcl  12715  zmin  12968  elpq  12999  qbtwnxr  13224  qsqueeze  13225  qextltlem  13226  xrsupsslem  13331  xrinfmsslem  13332  xrub  13336  supxrunb1  13343  ssnn0fi  14008  fsuppmapnn0fiub0  14016  fsuppmapnn0fz  14019  expnlbnd2  14256  r19.29uz  15372  cau3lem  15376  rlim2lt  15516  rlimclim  15565  2clim  15591  o1co  15605  climcn1  15611  climcn2  15612  rlimo1  15636  climsqz  15660  climsqz2  15661  rlimsqzlem  15668  lo1le  15671  climsup  15689  climcau  15690  caucvgrlem2  15694  iseralt  15704  cvgcmp  15835  cvgcmpce  15837  supcvg  15875  rpnnen2lem12  16244  bezoutlem1  16559  divgcdcoprmex  16686  exprmfct  16724  prmdvdsfz  16725  prmdvdsncoprmbd  16747  pclem  16859  pc2dvds  16900  pcprmpw  16904  dvdsprmpweqle  16907  unbenlem  16929  infpnlem2  16932  infpn2  16934  prmunb  16935  vdwlem2  17003  ramub1lem2  17048  prmdvdsprmop  17064  prmgaplem7  17078  ipodrsima  18556  smndex1mgm  18890  grpinveu  18962  dfgrp3lem  19026  psgneu  19493  odbezout  19545  sylow2blem3  19609  nn0gsumfz  19971  irredrmul  20396  zrninitoringc  20645  lbsextlem2  21130  znunit  21537  mptcoe1fsupp  22166  evls1fpws  22322  scmate  22465  scmatscm  22468  scmatfo  22485  mat1scmat  22494  pmatcoe1fsupp  22656  pmatcollpwfi  22737  pmatcollpw3fi  22740  mptcoe1matfsupp  22757  pm2mp  22780  chmaidscmat  22803  cpmadumatpoly  22838  chcoeffeq  22841  cayhamlem3  22842  cayhamlem4  22843  neiptopnei  23087  neitr  23135  cnpnei  23219  haust1  23307  isnrm3  23314  isreg2  23332  tgcmp  23356  hauscmplem  23361  hauscmp  23362  bwth  23365  1stcfb  23400  1stcelcls  23416  lly1stc  23451  txcmplem1  23596  txlm  23603  xkococnlem  23614  filuni  23840  filufint  23875  ufilen  23885  fclscf  23980  cnextcn  24022  ustex2sym  24172  ustex3sym  24173  utopreg  24208  isucn2  24234  ucnima  24236  ucncn  24240  neipcfilu  24251  metequiv2  24468  metrest  24482  xrsmopn  24771  mulc1cncf  24868  cncfco  24870  bndth  24927  lmmcvg  25232  cfil3i  25240  iscau4  25250  cmetcaulem  25259  iscmet3lem1  25262  caussi  25268  equivcfil  25270  equivcau  25271  caubl  25279  minveclem3b  25399  ovolgelb  25452  ovollb2lem  25460  ovolctb  25462  ovolicc2lem4  25492  ioombl1lem4  25533  dyadmax  25570  volsup2  25577  itg2monolem1  25722  c1liplem1  25972  c1lip1  25973  dvivthlem1  25984  lhop1  25990  ftc1a  26015  ftc1lem6  26019  ply1divex  26113  elply2  26172  dgrlem  26205  aacjcl  26306  aalioulem2  26312  aalioulem3  26313  aalioulem4  26314  ulmcaulem  26374  ulmcau  26375  ulmss  26377  mtest  26384  itgulm  26388  reeff1o  26428  efif1olem4  26524  rlimcnp  26945  xrlimcnp  26948  lgamucov  27018  ftalem3  27055  fta  27060  muval1  27113  dvdssqf  27118  mumullem1  27159  lgsqrmod  27333  lgsqrmodndvds  27334  pntlem3  27590  ostth  27620  nosupno  27685  nosupbnd1lem4  27693  noinfno  27700  noinfbnd1lem4  27708  conway  27781  etasslt  27795  znegscl  28315  tgtrisegint  28444  tgbtwndiff  28451  tgcgrxfr  28463  lnext  28512  legov2  28531  legtrd  28534  hlcgrex  28561  colperpexlem3  28677  colperpex  28678  hlpasch  28701  hpgerlem  28710  hpgtr  28713  dfcgra2  28775  acopy  28778  inagswap  28786  inaghl  28790  cgrg3col4  28798  axpasch  28887  wwlksnredwwlkn0  29845  midwwlks2s3  29901  clwwlkn1loopb  29991  2pthfrgrrn2  30231  frgrwopreg1  30266  frgrwopreg2  30267  grpoidinvlem3  30454  grpoideu  30457  grpoinveu  30467  ubthlem1  30818  minvecolem5  30829  htthlem  30865  chscllem2  31586  nmopun  31962  lnconi  31981  rnbra  32055  sumdmdii  32363  cdj3lem2b  32385  foresf1o  32452  acunirnmpt  32605  xrofsup  32713  fprodex01  32772  mndlactfo  32976  mndractfo  32978  isarchi3  33138  erler  33213  isarchiofld  33292  dfufd2lem  33517  constrconj  33730  constrextdg2lem  33733  constrcjcl  33753  lmxrge0  33926  lmdvg  33927  esumlub  34036  esumfsup  34046  esumcvg  34062  ftc2re  34588  cusgr3cyclex  35116  cvmliftmolem2  35262  cvmlift2lem12  35294  satfv1  35343  satffunlem1lem2  35383  satffunlem2lem2  35386  satfv0fvfmla0  35393  ellcsrspsn  35621  r1peuqusdeg1  35623  wzel  35800  wsuclem  35801  btwndiff  36003  trisegint  36004  cgrxfr  36031  lineext  36052  segcon2  36081  brsegle2  36085  seglecgr12im  36086  segletr  36090  broutsideof3  36102  opnrebl2  36297  nn0prpw  36299  fin2so  37589  poimirlem27  37629  poimirlem30  37632  poimirlem31  37633  poimir  37635  mblfinlem1  37639  mblfinlem2  37640  mblfinlem3  37641  mblfinlem4  37642  itg2addnclem  37653  ftc1cnnc  37674  ftc1anclem5  37679  sdclem1  37725  geomcau  37741  equivtotbnd  37760  bndss  37768  ismtybndlem  37788  heibor1lem  37791  rrncmslem  37814  rngo2  37889  prtlem15  38851  lsateln0  38971  lsat0cv  39009  eqlkr3  39077  lkrshp  39081  lshpset2N  39095  hlhgt2  39366  hlrelat2  39380  atle  39413  athgt  39433  2dim  39447  1cvratex  39450  ps-2  39455  dalem20  39670  lhpexle1lem  39984  lhpexle1  39985  lhpexle2lem  39986  lhpmcvr5N  40004  lhpmcvr6N  40005  cdleme25a  40330  cdleme29ex  40351  cdlemfnid  40541  cdlemg33b0  40678  cdlemg33a  40683  cdlemg35  40690  cdleml3N  40955  dihlsscpre  41211  dih1dimb2  41218  dihatexv  41315  dvh3dim2  41425  dochkr1  41455  dochkr1OLDN  41456  lcfl8  41479  lcfl8b  41481  lcfrlem5  41523  lcfrlem6  41524  mapdrvallem2  41622  mapdh9a  41766  mapdh9aOLDN  41767  hdmaprnlem3eN  41835  hdmaprnlem16N  41839  mndmolinv  42071  primrootsunit1  42073  flt4lem5elem  42640  flt4lem7  42648  nna4b4nsq  42649  fphpdo  42806  rencldnfilem  42809  irrapxlem2  42812  oasubex  43276  tfsconcatlem  43326  tfsconcatrev  43338  cvgdvgrat  44304  expgrowth  44326  projf1o  45174  ssfiunibd  45293  supxrgere  45316  supxrgelem  45320  suplesup  45322  infrpge  45334  infleinf  45355  supxrunb3  45382  unb2ltle  45398  uzub  45414  cvgcaule  45474  qinioo  45520  qelioo  45531  climinf  45593  mullimc  45603  islptre  45606  limccog  45607  mullimcf  45610  limcrecl  45616  sumnnodd  45617  neglimc  45634  0ellimcdiv  45636  limclner  45638  allbutfifvre  45662  climleltrp  45663  fnlimabslt  45666  climinf2lem  45693  limsuppnflem  45697  limsupvaluz2  45725  supcnvlimsup  45727  limsupgtlem  45764  liminflelimsupuz  45772  liminflimsupclim  45794  limsupub2  45799  xlimpnfxnegmnf  45801  cncfioobd  45884  stoweidlem7  45994  stoweidlem27  46014  stoweidlem39  46026  stoweidlem48  46035  stoweidlem49  46036  stoweidlem60  46047  stoweidlem61  46048  stoweid  46050  dirkercncflem2  46091  fourierdlem20  46114  fourierdlem39  46133  fourierdlem41  46135  fourierdlem48  46141  fourierdlem49  46142  fourierdlem50  46143  fourierdlem64  46157  fourierdlem73  46166  fourierdlem74  46167  fourierdlem75  46168  fourierdlem87  46180  fourierdlem103  46196  fourierdlem104  46197  qndenserrnopnlem  46284  sge0ltfirp  46387  sge0gerpmpt  46389  sge0ltfirpmpt2  46413  sge0isum  46414  sge0pnffigtmpt  46427  sge0pnffsumgt  46429  sge0gtfsumgt  46430  sge0uzfsumgt  46431  nnfoctbdjlem  46442  meaiuninclem  46467  meaiuninc3v  46471  omeiunltfirp  46506  carageniuncllem2  46509  hoicvr  46535  volicorescl  46540  hoidmv1le  46581  hoidmvlelem3  46584  hoiqssbllem3  46611  hspmbllem2  46614  iunhoiioolem  46662  vonioo  46669  vonicc  46672  smfaddlem1  46750  smflimlem2  46759  smflimlem3  46760  smfmullem4  46781  fsetsnfo  47038  2reu8i  47098  imasetpreimafvbijlemfo  47365  2pwp1prmfmtno  47550  proththd  47574  sbgoldbwt  47737  sbgoldbst  47738  sbgoldbalt  47741  bgoldbtbndlem4  47768  bgoldbtbnd  47769  grtriprop  47881  ply1mulgsumlem3  48278  ply1mulgsumlem4  48279  islindeps2  48373  isldepslvec2  48375