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  5640  frpomin  6321  dffo4  7078  nnaordex  8601  frfi  9222  fisupg  9225  marypha1  9373  fiinfg  9440  wemapsolem  9491  unwdomg  9525  rankr1ai  9749  cofsmo  10219  cfcoflem  10222  inar1  10726  nqerf  10881  prlem936  10998  fimaxre  12129  fiminre  12132  arch  12471  bndndx  12473  suprfinzcl  12680  zmin  12938  elpq  12969  qbtwnxr  13196  qsqueeze  13197  qextltlem  13198  xrsupsslem  13303  xrinfmsslem  13304  xrub  13308  supxrunb1  13315  ssnn0fi  13991  fsuppmapnn0fiub0  13999  fsuppmapnn0fz  14002  expnlbnd2  14240  r19.29uz  15368  cau3lem  15372  rlim2lt  15514  rlimclim  15563  2clim  15589  o1co  15603  climcn1  15609  climcn2  15610  rlimo1  15634  climsqz  15658  climsqz2  15659  rlimsqzlem  15666  lo1le  15669  climsup  15687  climcau  15688  caucvgrlem2  15692  iseralt  15702  cvgcmp  15834  cvgcmpce  15836  supcvg  15876  rpnnen2lem12  16247  bezoutlem1  16563  divgcdcoprmex  16690  exprmfct  16729  prmdvdsfz  16730  prmdvdsncoprmbd  16752  pclem  16864  pc2dvds  16905  pcprmpw  16909  dvdsprmpweqle  16912  unbenlem  16934  infpnlem2  16937  infpn2  16939  prmunb  16940  vdwlem2  17008  ramub1lem2  17053  prmdvdsprmop  17069  prmgaplem7  17083  ipodrsima  18563  smndex1mgm  18934  grpinveu  19006  dfgrp3lem  19070  psgneu  19536  odbezout  19588  sylow2blem3  19652  nn0gsumfz  20014  irredrmul  20462  zrninitoringc  20712  lbsextlem2  21216  znunit  21602  mptcoe1fsupp  22264  evls1fpws  22419  scmate  22557  scmatscm  22560  scmatfo  22577  mat1scmat  22586  pmatcoe1fsupp  22748  pmatcollpwfi  22829  pmatcollpw3fi  22832  mptcoe1matfsupp  22849  pm2mp  22872  chmaidscmat  22895  cpmadumatpoly  22930  chcoeffeq  22933  cayhamlem3  22934  cayhamlem4  22935  neiptopnei  23179  neitr  23227  cnpnei  23311  haust1  23399  isnrm3  23406  isreg2  23424  tgcmp  23448  hauscmplem  23453  hauscmp  23454  bwth  23457  1stcfb  23492  1stcelcls  23508  lly1stc  23543  txcmplem1  23688  txlm  23695  xkococnlem  23706  filuni  23932  filufint  23967  ufilen  23977  fclscf  24072  cnextcn  24114  ustex2sym  24264  ustex3sym  24265  utopreg  24299  isucn2  24325  ucnima  24327  ucncn  24331  neipcfilu  24342  metequiv2  24557  metrest  24571  xrsmopn  24860  mulc1cncf  24954  cncfco  24956  bndth  25007  lmmcvg  25310  cfil3i  25318  iscau4  25328  cmetcaulem  25337  iscmet3lem1  25340  caussi  25346  equivcfil  25348  equivcau  25349  caubl  25357  minveclem3b  25477  ovolgelb  25529  ovollb2lem  25537  ovolctb  25539  ovolicc2lem4  25569  ioombl1lem4  25610  dyadmax  25647  volsup2  25654  itg2monolem1  25799  c1liplem1  26045  c1lip1  26046  dvivthlem1  26057  lhop1  26063  ftc1a  26086  ftc1lem6  26090  ply1divex  26184  elply2  26243  dgrlem  26276  aacjcl  26378  aalioulem2  26384  aalioulem3  26385  aalioulem4  26386  ulmcaulem  26444  ulmcau  26445  ulmss  26447  mtest  26454  itgulm  26458  reeff1o  26497  efif1olem4  26597  rlimcnp  27017  xrlimcnp  27020  lgamucov  27089  ftalem3  27126  fta  27131  muval1  27184  dvdssqf  27189  mumullem1  27230  lgsqrmod  27403  lgsqrmodndvds  27404  pntlem3  27660  ostth  27690  nosupno  27754  nosupbnd1lem4  27762  noinfno  27769  noinfbnd1lem4  27777  conway  27859  etaslts  27873  znegscl  28472  tgtrisegint  28655  tgbtwndiff  28662  tgcgrxfr  28674  lnext  28723  legov2  28742  legtrd  28745  hlcgrex  28772  colperpexlem3  28888  colperpex  28889  hlpasch  28912  hpgerlem  28921  hpgtr  28924  dfcgra2  28986  acopy  28989  inagswap  28997  inaghl  29001  cgrg3col4  29009  axpasch  29098  wwlksnredwwlkn0  30052  midwwlks2s3  30108  clwwlkn1loopb  30201  2pthfrgrrn2  30441  frgrwopreg1  30476  frgrwopreg2  30477  grpoidinvlem3  30665  grpoideu  30668  grpoinveu  30678  ubthlem1  31029  minvecolem5  31040  htthlem  31076  chscllem2  31797  nmopun  32173  lnconi  32192  rnbra  32266  sumdmdii  32574  cdj3lem2b  32596  foresf1o  32662  acunirnmpt  32821  xrofsup  32929  fprodex01  32987  mndlactfo  33165  mndractfo  33167  isarchi3  33327  isarchiofld  33339  erler  33406  erld2  33407  dfufd2lem  33705  constrconj  34002  constrextdg2lem  34005  constrcjcl  34025  lmxrge0  34209  lmdvg  34210  esumlub  34317  esumfsup  34327  esumcvg  34343  ftc2re  34852  cusgr3cyclex  35446  cvmliftmolem2  35592  cvmlift2lem12  35624  satfv1  35673  satffunlem1lem2  35713  satffunlem2lem2  35716  satfv0fvfmla0  35723  ellcsrspsn  35951  r1peuqusdeg1  35953  wzel  36132  wsuclem  36133  btwndiff  36337  trisegint  36338  cgrxfr  36365  lineext  36386  segcon2  36415  brsegle2  36419  seglecgr12im  36420  segletr  36424  broutsideof3  36436  opnrebl2  36641  nn0prpw  36643  fin2so  38066  poimirlem27  38106  poimirlem30  38109  poimirlem31  38110  poimir  38112  mblfinlem1  38116  mblfinlem2  38117  mblfinlem3  38118  mblfinlem4  38119  itg2addnclem  38130  ftc1cnnc  38151  ftc1anclem5  38156  sdclem1  38202  geomcau  38218  equivtotbnd  38237  bndss  38245  ismtybndlem  38265  heibor1lem  38268  rrncmslem  38291  rngo2  38366  prtlem15  39459  lsateln0  39579  lsat0cv  39617  eqlkr3  39685  lkrshp  39689  lshpset2N  39703  hlhgt2  39973  hlrelat2  39987  atle  40020  athgt  40040  2dim  40054  1cvratex  40057  ps-2  40062  dalem20  40277  lhpexle1lem  40591  lhpexle1  40592  lhpexle2lem  40593  lhpmcvr5N  40611  lhpmcvr6N  40612  cdleme25a  40937  cdleme29ex  40958  cdlemfnid  41148  cdlemg33b0  41285  cdlemg33a  41290  cdlemg35  41297  cdleml3N  41562  dihlsscpre  41818  dih1dimb2  41825  dihatexv  41922  dvh3dim2  42032  dochkr1  42062  dochkr1OLDN  42063  lcfl8  42086  lcfl8b  42088  lcfrlem5  42130  lcfrlem6  42131  mapdrvallem2  42229  mapdh9a  42373  mapdh9aOLDN  42374  hdmaprnlem3eN  42442  hdmaprnlem16N  42446  mndmolinv  42672  primrootsunit1  42674  flt4lem5elem  43193  flt4lem7  43201  nna4b4nsq  43202  fphpdo  43354  rencldnfilem  43357  irrapxlem2  43360  oasubex  43823  tfsconcatlem  43873  tfsconcatrev  43885  cvgdvgrat  44849  expgrowth  44871  projf1o  45734  ssfiunibd  45848  supxrgere  45869  supxrgelem  45873  suplesup  45875  infrpge  45887  infleinf  45907  supxrunb3  45934  unb2ltle  45949  uzub  45965  cvgcaule  46025  qinioo  46071  qelioo  46082  climinf  46142  mullimc  46152  islptre  46155  limccog  46156  mullimcf  46159  limcrecl  46165  sumnnodd  46166  neglimc  46181  0ellimcdiv  46183  limclner  46185  allbutfifvre  46209  climleltrp  46210  fnlimabslt  46213  climinf2lem  46240  limsuppnflem  46244  limsupvaluz2  46272  supcnvlimsup  46274  limsupgtlem  46311  liminflelimsupuz  46319  liminflimsupclim  46341  limsupub2  46346  xlimpnfxnegmnf  46348  cncfioobd  46431  stoweidlem7  46541  stoweidlem27  46561  stoweidlem39  46573  stoweidlem48  46582  stoweidlem49  46583  stoweidlem60  46594  stoweidlem61  46595  stoweid  46597  dirkercncflem2  46638  fourierdlem20  46661  fourierdlem39  46680  fourierdlem41  46682  fourierdlem48  46688  fourierdlem49  46689  fourierdlem50  46690  fourierdlem64  46704  fourierdlem73  46713  fourierdlem74  46714  fourierdlem75  46715  fourierdlem87  46727  fourierdlem103  46743  fourierdlem104  46744  qndenserrnopnlem  46831  sge0ltfirp  46934  sge0gerpmpt  46936  sge0ltfirpmpt2  46960  sge0isum  46961  sge0pnffigtmpt  46974  sge0pnffsumgt  46976  sge0gtfsumgt  46977  sge0uzfsumgt  46978  nnfoctbdjlem  46989  meaiuninclem  47014  meaiuninc3v  47018  omeiunltfirp  47053  carageniuncllem2  47056  volicorescl  47087  hoidmv1le  47128  hoidmvlelem3  47131  hoiqssbllem3  47158  hspmbllem2  47161  iunhoiioolem  47209  vonioo  47216  vonicc  47219  smfaddlem1  47297  smflimlem2  47306  smflimlem3  47307  smfmullem4  47328  fsetsnfo  47607  2reu8i  47667  imasetpreimafvbijlemfo  47971  2pwp1prmfmtno  48159  proththd  48183  sbgoldbwt  48359  sbgoldbst  48360  sbgoldbalt  48363  bgoldbtbndlem4  48390  bgoldbtbnd  48391  grtriprop  48523  ply1mulgsumlem3  48970  ply1mulgsumlem4  48971  islindeps2  49065  isldepslvec2  49067