Theorem reximdva 3174

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-rex 3086

This theorem is referenced by:  reximddv  3177  reximdvva  3209  reximddv2  3220  wereu2  5642  frpomin  6323  dffo4  7080  nnaordex  8603  frfi  9225  fisupg  9228  marypha1  9377  fiinfg  9444  wemapsolem  9495  unwdomg  9529  rankr1ai  9753  cofsmo  10223  cfcoflem  10226  inar1  10730  nqerf  10885  prlem936  11002  fimaxre  12133  fiminre  12136  arch  12475  bndndx  12477  suprfinzcl  12684  zmin  12942  elpq  12973  qbtwnxr  13200  qsqueeze  13201  qextltlem  13202  xrsupsslem  13307  xrinfmsslem  13308  xrub  13312  supxrunb1  13319  ssnn0fi  13995  fsuppmapnn0fiub0  14003  fsuppmapnn0fz  14006  expnlbnd2  14244  r19.29uz  15361  cau3lem  15365  rlim2lt  15507  rlimclim  15556  2clim  15582  o1co  15596  climcn1  15602  climcn2  15603  rlimo1  15627  climsqz  15651  climsqz2  15652  rlimsqzlem  15659  lo1le  15662  climsup  15680  climcau  15681  caucvgrlem2  15685  iseralt  15695  cvgcmp  15827  cvgcmpce  15829  supcvg  15869  rpnnen2lem12  16240  bezoutlem1  16556  divgcdcoprmex  16683  exprmfct  16722  prmdvdsfz  16723  prmdvdsncoprmbd  16745  pclem  16857  pc2dvds  16898  pcprmpw  16902  dvdsprmpweqle  16905  unbenlem  16927  infpnlem2  16930  infpn2  16932  prmunb  16933  vdwlem2  17001  ramub1lem2  17046  prmdvdsprmop  17062  prmgaplem7  17076  ipodrsima  18556  smndex1mgm  18927  grpinveu  18999  dfgrp3lem  19063  psgneu  19529  odbezout  19581  sylow2blem3  19645  nn0gsumfz  20007  irredrmul  20455  zrninitoringc  20705  lbsextlem2  21209  znunit  21595  mptcoe1fsupp  22257  evls1fpws  22412  scmate  22550  scmatscm  22553  scmatfo  22570  mat1scmat  22579  pmatcoe1fsupp  22741  pmatcollpwfi  22822  pmatcollpw3fi  22825  mptcoe1matfsupp  22842  pm2mp  22865  chmaidscmat  22888  cpmadumatpoly  22923  chcoeffeq  22926  cayhamlem3  22927  cayhamlem4  22928  neiptopnei  23172  neitr  23220  cnpnei  23304  haust1  23392  isnrm3  23399  isreg2  23417  tgcmp  23441  hauscmplem  23446  hauscmp  23447  bwth  23450  1stcfb  23485  1stcelcls  23501  lly1stc  23536  txcmplem1  23681  txlm  23688  xkococnlem  23699  filuni  23925  filufint  23960  ufilen  23970  fclscf  24065  cnextcn  24107  ustex2sym  24257  ustex3sym  24258  utopreg  24292  isucn2  24318  ucnima  24320  ucncn  24324  neipcfilu  24335  metequiv2  24550  metrest  24564  xrsmopn  24853  mulc1cncf  24947  cncfco  24949  bndth  25000  lmmcvg  25303  cfil3i  25311  iscau4  25321  cmetcaulem  25330  iscmet3lem1  25333  caussi  25339  equivcfil  25341  equivcau  25342  caubl  25350  minveclem3b  25470  ovolgelb  25522  ovollb2lem  25530  ovolctb  25532  ovolicc2lem4  25562  ioombl1lem4  25603  dyadmax  25640  volsup2  25647  itg2monolem1  25792  c1liplem1  26038  c1lip1  26039  dvivthlem1  26050  lhop1  26056  ftc1a  26079  ftc1lem6  26083  ply1divex  26177  elply2  26236  dgrlem  26269  aacjcl  26368  aalioulem2  26374  aalioulem3  26375  aalioulem4  26376  ulmcaulem  26434  ulmcau  26435  ulmss  26437  mtest  26444  itgulm  26448  reeff1o  26487  efif1olem4  26587  rlimcnp  27007  xrlimcnp  27010  lgamucov  27079  ftalem3  27116  fta  27121  muval1  27174  dvdssqf  27179  mumullem1  27220  lgsqrmod  27393  lgsqrmodndvds  27394  pntlem3  27650  ostth  27680  nosupno  27744  nosupbnd1lem4  27752  noinfno  27759  noinfbnd1lem4  27767  conway  27849  etaslts  27863  znegscl  28462  tgtrisegint  28645  tgbtwndiff  28652  tgcgrxfr  28664  lnext  28713  legov2  28732  legtrd  28735  hlcgrex  28762  colperpexlem3  28878  colperpex  28879  hlpasch  28902  hpgerlem  28911  hpgtr  28914  dfcgra2  28976  acopy  28979  inagswap  28987  inaghl  28991  cgrg3col4  28999  axpasch  29088  wwlksnredwwlkn0  30042  midwwlks2s3  30098  clwwlkn1loopb  30191  2pthfrgrrn2  30431  frgrwopreg1  30466  frgrwopreg2  30467  grpoidinvlem3  30655  grpoideu  30658  grpoinveu  30668  ubthlem1  31019  minvecolem5  31030  htthlem  31066  chscllem2  31787  nmopun  32163  lnconi  32182  rnbra  32256  sumdmdii  32564  cdj3lem2b  32586  foresf1o  32652  acunirnmpt  32811  xrofsup  32919  fprodex01  32977  mndlactfo  33166  mndractfo  33168  isarchi3  33328  isarchiofld  33340  erler  33407  erld2  33408  dfufd2lem  33706  constrconj  34003  constrextdg2lem  34006  constrcjcl  34026  lmxrge0  34210  lmdvg  34211  esumlub  34318  esumfsup  34328  esumcvg  34344  ftc2re  34856  cusgr3cyclex  35450  cvmliftmolem2  35596  cvmlift2lem12  35628  satfv1  35677  satffunlem1lem2  35717  satffunlem2lem2  35720  satfv0fvfmla0  35727  ellcsrspsn  35955  r1peuqusdeg1  35957  wzel  36136  wsuclem  36137  btwndiff  36341  trisegint  36342  cgrxfr  36369  lineext  36390  segcon2  36419  brsegle2  36423  seglecgr12im  36424  segletr  36428  broutsideof3  36440  opnrebl2  36645  nn0prpw  36647  fin2so  38070  poimirlem27  38110  poimirlem30  38113  poimirlem31  38114  poimir  38116  mblfinlem1  38120  mblfinlem2  38121  mblfinlem3  38122  mblfinlem4  38123  itg2addnclem  38134  ftc1cnnc  38155  ftc1anclem5  38160  sdclem1  38206  geomcau  38222  equivtotbnd  38241  bndss  38249  ismtybndlem  38269  heibor1lem  38272  rrncmslem  38295  rngo2  38370  prtlem15  39463  lsateln0  39583  lsat0cv  39621  eqlkr3  39689  lkrshp  39693  lshpset2N  39707  hlhgt2  39977  hlrelat2  39991  atle  40024  athgt  40044  2dim  40058  1cvratex  40061  ps-2  40066  dalem20  40281  lhpexle1lem  40595  lhpexle1  40596  lhpexle2lem  40597  lhpmcvr5N  40615  lhpmcvr6N  40616  cdleme25a  40941  cdleme29ex  40962  cdlemfnid  41152  cdlemg33b0  41289  cdlemg33a  41294  cdlemg35  41301  cdleml3N  41566  dihlsscpre  41822  dih1dimb2  41829  dihatexv  41926  dvh3dim2  42036  dochkr1  42066  dochkr1OLDN  42067  lcfl8  42090  lcfl8b  42092  lcfrlem5  42134  lcfrlem6  42135  mapdrvallem2  42233  mapdh9a  42377  mapdh9aOLDN  42378  hdmaprnlem3eN  42446  hdmaprnlem16N  42450  mndmolinv  42676  primrootsunit1  42678  flt4lem5elem  43197  flt4lem7  43205  nna4b4nsq  43206  fphpdo  43358  rencldnfilem  43361  irrapxlem2  43364  oasubex  43827  tfsconcatlem  43877  tfsconcatrev  43889  cvgdvgrat  44853  expgrowth  44875  projf1o  45738  ssfiunibd  45852  supxrgere  45873  supxrgelem  45877  suplesup  45879  infrpge  45891  infleinf  45911  supxrunb3  45938  unb2ltle  45953  uzub  45969  cvgcaule  46029  qinioo  46075  qelioo  46086  climinf  46146  mullimc  46156  islptre  46159  limccog  46160  mullimcf  46163  limcrecl  46169  sumnnodd  46170  neglimc  46185  0ellimcdiv  46187  limclner  46189  allbutfifvre  46213  climleltrp  46214  fnlimabslt  46217  climinf2lem  46244  limsuppnflem  46248  limsupvaluz2  46276  supcnvlimsup  46278  limsupgtlem  46315  liminflelimsupuz  46323  liminflimsupclim  46345  limsupub2  46350  xlimpnfxnegmnf  46352  cncfioobd  46435  stoweidlem7  46545  stoweidlem27  46565  stoweidlem39  46577  stoweidlem48  46586  stoweidlem49  46587  stoweidlem60  46598  stoweidlem61  46599  stoweid  46601  dirkercncflem2  46642  fourierdlem20  46665  fourierdlem39  46684  fourierdlem41  46686  fourierdlem48  46692  fourierdlem49  46693  fourierdlem50  46694  fourierdlem64  46708  fourierdlem73  46717  fourierdlem74  46718  fourierdlem75  46719  fourierdlem87  46731  fourierdlem103  46747  fourierdlem104  46748  qndenserrnopnlem  46835  sge0ltfirp  46938  sge0gerpmpt  46940  sge0ltfirpmpt2  46964  sge0isum  46965  sge0pnffigtmpt  46978  sge0pnffsumgt  46980  sge0gtfsumgt  46981  sge0uzfsumgt  46982  nnfoctbdjlem  46993  meaiuninclem  47018  meaiuninc3v  47022  omeiunltfirp  47057  carageniuncllem2  47060  volicorescl  47091  hoidmv1le  47132  hoidmvlelem3  47135  hoiqssbllem3  47162  hspmbllem2  47165  iunhoiioolem  47213  vonioo  47220  vonicc  47223  smfaddlem1  47301  smflimlem2  47310  smflimlem3  47311  smfmullem4  47332  fsetsnfo  47611  2reu8i  47671  imasetpreimafvbijlemfo  47975  2pwp1prmfmtno  48163  proththd  48187  sbgoldbwt  48363  sbgoldbst  48364  sbgoldbalt  48367  bgoldbtbndlem4  48394  bgoldbtbnd  48395  grtriprop  48527  ply1mulgsumlem3  48974  ply1mulgsumlem4  48975  islindeps2  49069  isldepslvec2  49071