Theorem reximdva 3203

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∃wrex 3065

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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-rex 3070

This theorem is referenced by:  reximddv  3204  reximdvva  3206  reximddv2  3207  wereu2  5586  frpomin  6243  dffo4  6979  nnaordex  8469  frfi  9059  fisupg  9062  marypha1  9193  fiinfg  9258  wemapsolem  9309  unwdomg  9343  rankr1ai  9556  cofsmo  10025  cfcoflem  10028  inar1  10531  nqerf  10686  prlem936  10803  fimaxre  11919  fiminre  11922  arch  12230  bndndx  12232  suprfinzcl  12436  zmin  12684  elpq  12715  qbtwnxr  12934  qsqueeze  12935  qextltlem  12936  xrsupsslem  13041  xrinfmsslem  13042  xrub  13046  supxrunb1  13053  ssnn0fi  13705  fsuppmapnn0fiub0  13713  fsuppmapnn0fz  13716  expnlbnd2  13949  r19.29uz  15062  cau3lem  15066  rlim2lt  15206  rlimclim  15255  2clim  15281  o1co  15295  climcn1  15301  climcn2  15302  rlimo1  15326  climsqz  15350  climsqz2  15351  rlimsqzlem  15360  lo1le  15363  climsup  15381  climcau  15382  caucvgrlem2  15386  iseralt  15396  cvgcmp  15528  cvgcmpce  15530  supcvg  15568  rpnnen2lem12  15934  bezoutlem1  16247  divgcdcoprmex  16371  exprmfct  16409  prmdvdsfz  16410  prmdvdsncoprmbd  16431  pclem  16539  pc2dvds  16580  pcprmpw  16584  dvdsprmpweqle  16587  unbenlem  16609  infpnlem2  16612  infpn2  16614  prmunb  16615  vdwlem2  16683  ramub1lem2  16728  prmdvdsprmop  16744  prmgaplem7  16758  ipodrsima  18259  smndex1mgm  18546  grpinveu  18614  dfgrp3lem  18673  psgneu  19114  odbezout  19165  sylow2blem3  19227  nn0gsumfz  19585  ringadd2  19814  irredrmul  19949  lbsextlem2  20421  znunit  20771  mptcoe1fsupp  21386  scmate  21659  scmatscm  21662  scmatfo  21679  mat1scmat  21688  pmatcoe1fsupp  21850  pmatcollpwfi  21931  pmatcollpw3fi  21934  mptcoe1matfsupp  21951  pm2mp  21974  chmaidscmat  21997  cpmadumatpoly  22032  chcoeffeq  22035  cayhamlem3  22036  cayhamlem4  22037  neiptopnei  22283  neitr  22331  cnpnei  22415  haust1  22503  isnrm3  22510  isreg2  22528  tgcmp  22552  hauscmplem  22557  hauscmp  22558  bwth  22561  1stcfb  22596  1stcelcls  22612  lly1stc  22647  txcmplem1  22792  txlm  22799  xkococnlem  22810  filuni  23036  filufint  23071  ufilen  23081  fclscf  23176  cnextcn  23218  ustex2sym  23368  ustex3sym  23369  utopreg  23404  isucn2  23431  ucnima  23433  ucncn  23437  neipcfilu  23448  metequiv2  23666  metrest  23680  xrsmopn  23975  mulc1cncf  24068  cncfco  24070  bndth  24121  lmmcvg  24425  cfil3i  24433  iscau4  24443  cmetcaulem  24452  iscmet3lem1  24455  caussi  24461  equivcfil  24463  equivcau  24464  caubl  24472  minveclem3b  24592  ovolgelb  24644  ovollb2lem  24652  ovolctb  24654  ovolicc2lem4  24684  ioombl1lem4  24725  dyadmax  24762  volsup2  24769  itg2monolem1  24915  c1liplem1  25160  c1lip1  25161  dvivthlem1  25172  lhop1  25178  ftc1a  25201  ftc1lem6  25205  ply1divex  25301  elply2  25357  dgrlem  25390  aacjcl  25487  aalioulem2  25493  aalioulem3  25494  aalioulem4  25495  ulmcaulem  25553  ulmcau  25554  ulmss  25556  mtest  25563  itgulm  25567  reeff1o  25606  efif1olem4  25701  rlimcnp  26115  xrlimcnp  26118  lgamucov  26187  ftalem3  26224  fta  26229  muval1  26282  dvdssqf  26287  mumullem1  26328  lgsqrmod  26500  lgsqrmodndvds  26501  pntlem3  26757  ostth  26787  tgtrisegint  26860  tgbtwndiff  26867  tgcgrxfr  26879  lnext  26928  legov2  26947  legtrd  26950  hlcgrex  26977  colperpexlem3  27093  colperpex  27094  hlpasch  27117  hpgerlem  27126  hpgtr  27129  dfcgra2  27191  acopy  27194  inagswap  27202  inaghl  27206  cgrg3col4  27214  axpasch  27309  wwlksnredwwlkn0  28261  midwwlks2s3  28317  clwwlkn1loopb  28407  2pthfrgrrn2  28647  frgrwopreg1  28682  frgrwopreg2  28683  grpoidinvlem3  28868  grpoideu  28871  grpoinveu  28881  ubthlem1  29232  minvecolem5  29243  htthlem  29279  chscllem2  30000  nmopun  30376  lnconi  30395  rnbra  30469  sumdmdii  30777  cdj3lem2b  30799  foresf1o  30850  acunirnmpt  30996  xrofsup  31090  fprodex01  31139  isarchi3  31441  isarchiofld  31516  lmxrge0  31902  lmdvg  31903  esumlub  32028  esumfsup  32038  esumcvg  32054  ftc2re  32578  cusgr3cyclex  33098  cvmliftmolem2  33244  cvmlift2lem12  33276  satfv1  33325  satffunlem1lem2  33365  satffunlem2lem2  33368  satfv0fvfmla0  33375  wzel  33818  wsuclem  33819  nosupno  33906  nosupbnd1lem4  33914  noinfno  33921  noinfbnd1lem4  33929  conway  33993  etasslt  34007  btwndiff  34329  trisegint  34330  cgrxfr  34357  lineext  34378  segcon2  34407  brsegle2  34411  seglecgr12im  34412  segletr  34416  broutsideof3  34428  opnrebl2  34510  nn0prpw  34512  fin2so  35764  poimirlem27  35804  poimirlem30  35807  poimirlem31  35808  poimir  35810  mblfinlem1  35814  mblfinlem2  35815  mblfinlem3  35816  mblfinlem4  35817  itg2addnclem  35828  ftc1cnnc  35849  ftc1anclem5  35854  sdclem1  35901  geomcau  35917  equivtotbnd  35936  bndss  35944  ismtybndlem  35964  heibor1lem  35967  rrncmslem  35990  rngo2  36065  prtlem15  36889  lsateln0  37009  lsat0cv  37047  eqlkr3  37115  lkrshp  37119  lshpset2N  37133  hlhgt2  37403  hlrelat2  37417  atle  37450  athgt  37470  2dim  37484  1cvratex  37487  ps-2  37492  dalem20  37707  lhpexle1lem  38021  lhpexle1  38022  lhpexle2lem  38023  lhpmcvr5N  38041  lhpmcvr6N  38042  cdleme25a  38367  cdleme29ex  38388  cdlemfnid  38578  cdlemg33b0  38715  cdlemg33a  38720  cdlemg35  38727  cdleml3N  38992  dihlsscpre  39248  dih1dimb2  39255  dihatexv  39352  dvh3dim2  39462  dochkr1  39492  dochkr1OLDN  39493  lcfl8  39516  lcfl8b  39518  lcfrlem5  39560  lcfrlem6  39561  mapdrvallem2  39659  mapdh9a  39803  mapdh9aOLDN  39804  hdmaprnlem3eN  39872  hdmaprnlem16N  39876  flt4lem5elem  40488  flt4lem7  40496  nna4b4nsq  40497  fphpdo  40639  rencldnfilem  40642  irrapxlem2  40645  cvgdvgrat  41931  expgrowth  41953  projf1o  42736  ssfiunibd  42848  supxrgere  42872  supxrgelem  42876  suplesup  42878  infrpge  42890  infleinf  42911  supxrunb3  42939  unb2ltle  42955  uzub  42971  qinioo  43073  qelioo  43084  climinf  43147  mullimc  43157  islptre  43160  limccog  43161  mullimcf  43164  limcrecl  43170  sumnnodd  43171  neglimc  43188  0ellimcdiv  43190  limclner  43192  allbutfifvre  43216  climleltrp  43217  fnlimabslt  43220  climinf2lem  43247  limsuppnflem  43251  limsupvaluz2  43279  supcnvlimsup  43281  limsupgtlem  43318  liminflelimsupuz  43326  liminflimsupclim  43348  limsupub2  43353  xlimpnfxnegmnf  43355  cncfioobd  43438  stoweidlem7  43548  stoweidlem27  43568  stoweidlem39  43580  stoweidlem48  43589  stoweidlem49  43590  stoweidlem60  43601  stoweidlem61  43602  stoweid  43604  dirkercncflem2  43645  fourierdlem20  43668  fourierdlem39  43687  fourierdlem41  43689  fourierdlem48  43695  fourierdlem49  43696  fourierdlem50  43697  fourierdlem64  43711  fourierdlem73  43720  fourierdlem74  43721  fourierdlem75  43722  fourierdlem87  43734  fourierdlem103  43750  fourierdlem104  43751  qndenserrnopnlem  43838  sge0ltfirp  43938  sge0gerpmpt  43940  sge0ltfirpmpt2  43964  sge0isum  43965  sge0pnffigtmpt  43978  sge0pnffsumgt  43980  sge0gtfsumgt  43981  sge0uzfsumgt  43982  nnfoctbdjlem  43993  meaiuninclem  44018  meaiuninc3v  44022  omeiunltfirp  44057  carageniuncllem2  44060  hoicvr  44086  volicorescl  44091  hoidmv1le  44132  hoidmvlelem3  44135  hoiqssbllem3  44162  hspmbllem2  44165  iunhoiioolem  44213  vonioo  44220  vonicc  44223  smfaddlem1  44298  smflimlem2  44307  smflimlem3  44308  smfmullem4  44328  fsetsnfo  44547  2reu8i  44605  imasetpreimafvbijlemfo  44857  2pwp1prmfmtno  45042  proththd  45066  sbgoldbwt  45229  sbgoldbst  45230  sbgoldbalt  45233  bgoldbtbndlem4  45260  bgoldbtbnd  45261  zrninitoringc  45629  ply1mulgsumlem3  45729  ply1mulgsumlem4  45730  islindeps2  45824  isldepslvec2  45826