Theorem reximdva 3233

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  ∃wrex 3107

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 1911

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3111  df-rex 3112

This theorem is referenced by:  reximddv  3234  reximdvva  3236  reximddv2  3237  wereu2  5516  dffo4  6846  nnaordex  8247  frfi  8747  fisupg  8750  marypha1  8882  fiinfg  8947  wemapsolem  8998  unwdomg  9032  rankr1ai  9211  cofsmo  9680  cfcoflem  9683  inar1  10186  nqerf  10341  prlem936  10458  fimaxre  11573  fiminre  11576  arch  11882  bndndx  11884  suprfinzcl  12085  zmin  12332  elpq  12362  qbtwnxr  12581  qsqueeze  12582  qextltlem  12583  xrsupsslem  12688  xrinfmsslem  12689  xrub  12693  supxrunb1  12700  ssnn0fi  13348  fsuppmapnn0fiub0  13356  fsuppmapnn0fz  13359  expnlbnd2  13591  r19.29uz  14702  cau3lem  14706  rlim2lt  14846  rlimclim  14895  2clim  14921  o1co  14935  climcn1  14940  climcn2  14941  rlimo1  14965  climsqz  14989  climsqz2  14990  rlimsqzlem  14997  lo1le  15000  climsup  15018  climcau  15019  caucvgrlem2  15023  iseralt  15033  cvgcmp  15163  cvgcmpce  15165  supcvg  15203  rpnnen2lem12  15570  bezoutlem1  15877  divgcdcoprmex  16000  exprmfct  16038  prmdvdsfz  16039  pclem  16165  pc2dvds  16205  pcprmpw  16209  dvdsprmpweqle  16212  unbenlem  16234  infpnlem2  16237  infpn2  16239  prmunb  16240  vdwlem2  16308  ramub1lem2  16353  prmdvdsprmop  16369  prmgaplem7  16383  ipodrsima  17767  smndex1mgm  18064  grpinveu  18130  dfgrp3lem  18189  psgneu  18626  odbezout  18677  sylow2blem3  18739  nn0gsumfz  19097  ringadd2  19321  irredrmul  19453  lbsextlem2  19924  znunit  20255  mptcoe1fsupp  20844  scmate  21115  scmatscm  21118  scmatfo  21135  mat1scmat  21144  pmatcoe1fsupp  21306  pmatcollpwfi  21387  pmatcollpw3fi  21390  mptcoe1matfsupp  21407  pm2mp  21430  chmaidscmat  21453  cpmadumatpoly  21488  chcoeffeq  21491  cayhamlem3  21492  cayhamlem4  21493  neiptopnei  21737  neitr  21785  cnpnei  21869  haust1  21957  isnrm3  21964  isreg2  21982  tgcmp  22006  hauscmplem  22011  hauscmp  22012  bwth  22015  1stcfb  22050  1stcelcls  22066  lly1stc  22101  txcmplem1  22246  txlm  22253  xkococnlem  22264  filuni  22490  filufint  22525  ufilen  22535  fclscf  22630  cnextcn  22672  ustex2sym  22822  ustex3sym  22823  utopreg  22858  isucn2  22885  ucnima  22887  ucncn  22891  neipcfilu  22902  metequiv2  23117  metrest  23131  xrsmopn  23417  mulc1cncf  23510  cncfco  23512  bndth  23563  lmmcvg  23865  cfil3i  23873  iscau4  23883  cmetcaulem  23892  iscmet3lem1  23895  caussi  23901  equivcfil  23903  equivcau  23904  caubl  23912  minveclem3b  24032  ovolgelb  24084  ovollb2lem  24092  ovolctb  24094  ovolicc2lem4  24124  ioombl1lem4  24165  dyadmax  24202  volsup2  24209  itg2monolem1  24354  c1liplem1  24599  c1lip1  24600  dvivthlem1  24611  lhop1  24617  ftc1a  24640  ftc1lem6  24644  ply1divex  24737  elply2  24793  dgrlem  24826  aacjcl  24923  aalioulem2  24929  aalioulem3  24930  aalioulem4  24931  ulmcaulem  24989  ulmcau  24990  ulmss  24992  mtest  24999  itgulm  25003  reeff1o  25042  efif1olem4  25137  rlimcnp  25551  xrlimcnp  25554  lgamucov  25623  ftalem3  25660  fta  25665  muval1  25718  dvdssqf  25723  mumullem1  25764  lgsqrmod  25936  lgsqrmodndvds  25937  pntlem3  26193  ostth  26223  tgtrisegint  26293  tgbtwndiff  26300  tgcgrxfr  26312  lnext  26361  legov2  26380  legtrd  26383  hlcgrex  26410  colperpexlem3  26526  colperpex  26527  hlpasch  26550  hpgerlem  26559  hpgtr  26562  dfcgra2  26624  acopy  26627  inagswap  26635  inaghl  26639  cgrg3col4  26647  axpasch  26735  wwlksnredwwlkn0  27682  midwwlks2s3  27738  clwwlkn1loopb  27828  2pthfrgrrn2  28068  frgrwopreg1  28103  frgrwopreg2  28104  grpoidinvlem3  28289  grpoideu  28292  grpoinveu  28302  ubthlem1  28653  minvecolem5  28664  htthlem  28700  chscllem2  29421  nmopun  29797  lnconi  29816  rnbra  29890  sumdmdii  30198  cdj3lem2b  30220  foresf1o  30273  acunirnmpt  30422  xrofsup  30518  fprodex01  30567  isarchi3  30866  isarchiofld  30941  lmxrge0  31305  lmdvg  31306  esumlub  31429  esumfsup  31439  esumcvg  31455  ftc2re  31979  cusgr3cyclex  32496  cvmliftmolem2  32642  cvmlift2lem12  32674  satfv1  32723  satffunlem1lem2  32763  satffunlem2lem2  32766  satfv0fvfmla0  32773  frpomin  33191  frmin  33197  wzel  33224  wsuclem  33225  nosupno  33316  nosupbnd1lem4  33324  conway  33377  btwndiff  33601  trisegint  33602  cgrxfr  33629  lineext  33650  segcon2  33679  brsegle2  33683  seglecgr12im  33684  segletr  33688  broutsideof3  33700  opnrebl2  33782  nn0prpw  33784  fin2so  35044  poimirlem27  35084  poimirlem30  35087  poimirlem31  35088  poimir  35090  mblfinlem1  35094  mblfinlem2  35095  mblfinlem3  35096  mblfinlem4  35097  itg2addnclem  35108  ftc1cnnc  35129  ftc1anclem5  35134  sdclem1  35181  geomcau  35197  equivtotbnd  35216  bndss  35224  ismtybndlem  35244  heibor1lem  35247  rrncmslem  35270  rngo2  35345  prtlem15  36171  lsateln0  36291  lsat0cv  36329  eqlkr3  36397  lkrshp  36401  lshpset2N  36415  hlhgt2  36685  hlrelat2  36699  atle  36732  athgt  36752  2dim  36766  1cvratex  36769  ps-2  36774  dalem20  36989  lhpexle1lem  37303  lhpexle1  37304  lhpexle2lem  37305  lhpmcvr5N  37323  lhpmcvr6N  37324  cdleme25a  37649  cdleme29ex  37670  cdlemfnid  37860  cdlemg33b0  37997  cdlemg33a  38002  cdlemg35  38009  cdleml3N  38274  dihlsscpre  38530  dih1dimb2  38537  dihatexv  38634  dvh3dim2  38744  dochkr1  38774  dochkr1OLDN  38775  lcfl8  38798  lcfl8b  38800  lcfrlem5  38842  lcfrlem6  38843  mapdrvallem2  38941  mapdh9a  39085  mapdh9aOLDN  39086  hdmaprnlem3eN  39154  hdmaprnlem16N  39158  fphpdo  39758  rencldnfilem  39761  irrapxlem2  39764  cvgdvgrat  41017  expgrowth  41039  projf1o  41825  ssfiunibd  41941  supxrgere  41965  supxrgelem  41969  suplesup  41971  infrpge  41983  infleinf  42004  supxrunb3  42036  unb2ltle  42052  uzub  42068  qinioo  42172  qelioo  42183  climinf  42248  mullimc  42258  islptre  42261  limccog  42262  mullimcf  42265  limcrecl  42271  sumnnodd  42272  neglimc  42289  0ellimcdiv  42291  limclner  42293  allbutfifvre  42317  climleltrp  42318  fnlimabslt  42321  climinf2lem  42348  limsuppnflem  42352  limsupvaluz2  42380  supcnvlimsup  42382  limsupgtlem  42419  liminflelimsupuz  42427  liminflimsupclim  42449  limsupub2  42454  xlimpnfxnegmnf  42456  cncfioobd  42539  stoweidlem7  42649  stoweidlem27  42669  stoweidlem39  42681  stoweidlem48  42690  stoweidlem49  42691  stoweidlem60  42702  stoweidlem61  42703  stoweid  42705  dirkercncflem2  42746  fourierdlem20  42769  fourierdlem39  42788  fourierdlem41  42790  fourierdlem48  42796  fourierdlem49  42797  fourierdlem50  42798  fourierdlem64  42812  fourierdlem73  42821  fourierdlem74  42822  fourierdlem75  42823  fourierdlem87  42835  fourierdlem103  42851  fourierdlem104  42852  qndenserrnopnlem  42939  sge0ltfirp  43039  sge0gerpmpt  43041  sge0ltfirpmpt2  43065  sge0isum  43066  sge0pnffigtmpt  43079  sge0pnffsumgt  43081  sge0gtfsumgt  43082  sge0uzfsumgt  43083  nnfoctbdjlem  43094  meaiuninclem  43119  meaiuninc3v  43123  omeiunltfirp  43158  carageniuncllem2  43161  hoicvr  43187  volicorescl  43192  hoidmv1le  43233  hoidmvlelem3  43236  hoiqssbllem3  43263  hspmbllem2  43266  iunhoiioolem  43314  vonioo  43321  vonicc  43324  smfaddlem1  43396  smflimlem2  43405  smflimlem3  43406  smfmullem4  43426  2reu8i  43669  imasetpreimafvbijlemfo  43922  2pwp1prmfmtno  44107  proththd  44132  sbgoldbwt  44295  sbgoldbst  44296  sbgoldbalt  44299  bgoldbtbndlem4  44326  bgoldbtbnd  44327  zrninitoringc  44695  ply1mulgsumlem3  44796  ply1mulgsumlem4  44797  islindeps2  44892  isldepslvec2  44894