Theorem reximdva 3225

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
reximdva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))

Assertion

Ref	Expression
reximdva	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reximdva

Step	Hyp	Ref	Expression
1		reximdva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
2	1	ex 403	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	reximdvai 3223	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2164  ∃wrex 3118

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879  df-ral 3122  df-rex 3123

This theorem is referenced by:  reximddv  3226  reximdvva  3228  reximddv2  3229  wereu2  5339  dffo4  6624  nnaordex  7985  frfi  8474  fisupg  8477  marypha1  8609  fiinfg  8674  wemapsolem  8724  unwdomg  8758  rankr1ai  8938  cofsmo  9406  cfcoflem  9409  inar1  9912  nqerf  10067  prlem936  10184  fimaxre  11298  arch  11615  bndndx  11617  suprfinzcl  11820  zmin  12067  elpq  12097  qbtwnxr  12319  qsqueeze  12320  qextltlem  12321  xrsupsslem  12425  xrinfmsslem  12426  xrub  12430  supxrunb1  12437  ssnn0fi  13079  fsuppmapnn0fiub0  13087  fsuppmapnn0fz  13090  expnlbnd2  13289  r19.29uz  14467  cau3lem  14471  rlim2lt  14605  rlimclim  14654  2clim  14680  o1co  14694  climcn1  14699  climcn2  14700  rlimo1  14724  climsqz  14748  climsqz2  14749  rlimsqzlem  14756  lo1le  14759  climsup  14777  climcau  14778  caucvgrlem2  14782  iseralt  14792  cvgcmp  14922  cvgcmpce  14924  supcvg  14962  rpnnen2lem12  15328  bezoutlem1  15629  divgcdcoprmex  15752  exprmfct  15787  prmdvdsfz  15788  pclem  15914  pc2dvds  15954  pcprmpw  15958  dvdsprmpweqle  15961  unbenlem  15983  infpnlem2  15986  infpn2  15988  prmunb  15989  vdwlem2  16057  ramub1lem2  16102  prmdvdsprmop  16118  prmgaplem7  16132  ipodrsima  17518  grpinveu  17810  dfgrp3lem  17867  psgneu  18277  odbezout  18326  sylow2blem3  18388  nn0gsumfz  18733  ringadd2  18929  irredrmul  19061  lbsextlem2  19520  mptcoe1fsupp  19945  znunit  20271  scmate  20684  scmatscm  20687  scmatfo  20704  mat1scmat  20713  pmatcoe1fsupp  20876  pmatcollpwfi  20957  pmatcollpw3fi  20960  mptcoe1matfsupp  20977  pm2mp  21000  chmaidscmat  21023  cpmadumatpoly  21058  chcoeffeq  21061  cayhamlem3  21062  cayhamlem4  21063  neiptopnei  21307  neitr  21355  cnpnei  21439  haust1  21527  isnrm3  21534  isreg2  21552  tgcmp  21575  hauscmplem  21580  hauscmp  21581  bwth  21584  1stcfb  21619  1stcelcls  21635  lly1stc  21670  txcmplem1  21815  txlm  21822  xkococnlem  21833  filuni  22059  filufint  22094  ufilen  22104  fclscf  22199  cnextcn  22241  ustex2sym  22390  ustex3sym  22391  utopreg  22426  isucn2  22453  ucnima  22455  ucncn  22459  neipcfilu  22470  metequiv2  22685  metrest  22699  xrsmopn  22985  mulc1cncf  23078  cncfco  23080  bndth  23127  lmmcvg  23429  cfil3i  23437  iscau4  23447  cmetcaulem  23456  iscmet3lem1  23459  caussi  23465  equivcfil  23467  equivcau  23468  caubl  23476  minveclem3b  23596  ovolgelb  23646  ovollb2lem  23654  ovolctb  23656  ovolicc2lem4  23686  ioombl1lem4  23727  dyadmax  23764  volsup2  23771  itg2monolem1  23916  c1liplem1  24158  c1lip1  24159  dvivthlem1  24170  lhop1  24176  ftc1a  24199  ftc1lem6  24203  ply1divex  24295  elply2  24351  dgrlem  24384  aacjcl  24481  aalioulem2  24487  aalioulem3  24488  aalioulem4  24489  ulmcaulem  24547  ulmcau  24548  ulmss  24550  mtest  24557  itgulm  24561  reeff1o  24600  efif1olem4  24691  rlimcnp  25105  xrlimcnp  25108  lgamucov  25177  ftalem3  25214  fta  25219  muval1  25272  dvdssqf  25277  mumullem1  25318  lgsqrmod  25490  lgsqrmodndvds  25491  pntlem3  25711  ostth  25741  tgtrisegint  25811  tgbtwndiff  25818  tgcgrxfr  25830  lnext  25879  legov2  25898  legtrd  25901  hlcgrex  25928  colperpexlem3  26041  colperpex  26042  hlpasch  26065  hpgerlem  26074  hpgtr  26077  dfcgra2  26138  acopy  26142  inagswap  26148  inaghl  26149  cgrg3col4  26152  axpasch  26240  wwlksnredwwlkn0  27209  wwlksnredwwlkn0OLD  27210  midwwlks2s3  27281  clwwlkn1loopb  27382  2pthfrgrrn2  27653  frgrwopreg1  27688  frgrwopreg2  27689  grpoidinvlem3  27905  grpoideu  27908  grpoinveu  27918  ubthlem1  28270  minvecolem5  28281  htthlem  28318  chscllem2  29041  nmopun  29417  lnconi  29436  rnbra  29510  sumdmdii  29818  cdj3lem2b  29840  foresf1o  29880  acunirnmpt  29997  xrofsup  30069  fprodex01  30107  isarchi3  30275  isarchiofld  30351  lmxrge0  30532  lmdvg  30533  esumlub  30656  esumfsup  30666  esumcvg  30682  ftc2re  31214  cvmliftmolem2  31799  cvmlift2lem12  31831  frpomin  32266  frmin  32270  wzel  32297  wsuclem  32298  nosupno  32377  nosupbnd1lem4  32385  conway  32438  btwndiff  32662  trisegint  32663  cgrxfr  32690  lineext  32711  segcon2  32740  brsegle2  32744  seglecgr12im  32745  segletr  32749  broutsideof3  32761  opnrebl2  32843  nn0prpw  32845  fin2so  33932  poimirlem27  33973  poimirlem30  33976  poimirlem31  33977  poimir  33979  mblfinlem1  33983  mblfinlem2  33984  mblfinlem3  33985  mblfinlem4  33986  itg2addnclem  33997  ftc1cnnc  34020  ftc1anclem5  34025  sdclem1  34074  geomcau  34090  equivtotbnd  34112  bndss  34120  ismtybndlem  34140  heibor1lem  34143  rrncmslem  34166  rngo2  34241  prtlem15  34943  lsateln0  35063  lsat0cv  35101  eqlkr3  35169  lkrshp  35173  lshpset2N  35187  hlhgt2  35457  hlrelat2  35471  atle  35504  athgt  35524  2dim  35538  1cvratex  35541  ps-2  35546  dalem20  35761  lhpexle1lem  36075  lhpexle1  36076  lhpexle2lem  36077  lhpmcvr5N  36095  lhpmcvr6N  36096  cdleme25a  36421  cdleme29ex  36442  cdlemfnid  36632  cdlemg33b0  36769  cdlemg33a  36774  cdlemg35  36781  cdleml3N  37046  dihlsscpre  37302  dih1dimb2  37309  dihatexv  37406  dvh3dim2  37516  dochkr1  37546  dochkr1OLDN  37547  lcfl8  37570  lcfl8b  37572  lcfrlem5  37614  lcfrlem6  37615  mapdrvallem2  37713  mapdh9a  37857  mapdh9aOLDN  37858  hdmaprnlem3eN  37926  hdmaprnlem16N  37930  fphpdo  38218  rencldnfilem  38221  irrapxlem2  38224  cvgdvgrat  39345  expgrowth  39367  projf1o  40187  rnmptlb  40247  rnmptbddlem  40249  rnmptbd2lem  40256  ssfiunibd  40314  supxrgere  40339  supxrgelem  40343  suplesup  40345  infrpge  40357  infleinf  40378  supxrunb3  40411  unb2ltle  40430  uzub  40446  qinioo  40550  qelioo  40561  climinf  40626  mullimc  40636  islptre  40639  limccog  40640  mullimcf  40643  limcrecl  40649  sumnnodd  40650  neglimc  40667  0ellimcdiv  40669  limclner  40671  allbutfifvre  40695  climleltrp  40696  fnlimabslt  40699  climinf2lem  40726  limsuppnflem  40730  limsupvaluz2  40758  supcnvlimsup  40760  limsupgtlem  40797  liminflelimsupuz  40805  liminflimsupclim  40827  cncfioobd  40898  stoweidlem7  41011  stoweidlem27  41031  stoweidlem39  41043  stoweidlem48  41052  stoweidlem49  41053  stoweidlem60  41064  stoweidlem61  41065  stoweid  41067  dirkercncflem2  41108  fourierdlem20  41131  fourierdlem39  41150  fourierdlem41  41152  fourierdlem48  41158  fourierdlem49  41159  fourierdlem50  41160  fourierdlem64  41174  fourierdlem73  41183  fourierdlem74  41184  fourierdlem75  41185  fourierdlem87  41197  fourierdlem103  41213  fourierdlem104  41214  qndenserrnopnlem  41301  sge0ltfirp  41401  sge0gerpmpt  41403  sge0ltfirpmpt2  41427  sge0isum  41428  sge0pnffigtmpt  41441  sge0pnffsumgt  41443  sge0gtfsumgt  41444  sge0uzfsumgt  41445  nnfoctbdjlem  41456  meaiuninclem  41481  meaiuninc3v  41485  omeiunltfirp  41520  carageniuncllem2  41523  hoicvr  41549  volicorescl  41554  hoidmv1le  41595  hoidmvlelem3  41598  hoiqssbllem3  41625  hspmbllem2  41628  iunhoiioolem  41676  vonioo  41683  vonicc  41686  smfaddlem1  41758  smflimlem2  41767  smflimlem3  41768  smfmullem4  41788  2pwp1prmfmtno  42327  proththd  42354  sbgoldbwt  42488  sbgoldbst  42489  sbgoldbalt  42492  bgoldbtbndlem4  42519  bgoldbtbnd  42520  zrninitoringc  42911  ply1mulgsumlem3  43016  ply1mulgsumlem4  43017  islindeps2  43112  isldepslvec2  43114