Theorem reximdva 3168

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3071

This theorem is referenced by:  reximddv  3171  reximdvva  3207  reximddv2  3215  wereu2  5682  frpomin  6361  dffo4  7123  nnaordex  8676  frfi  9321  fisupg  9324  marypha1  9474  fiinfg  9539  wemapsolem  9590  unwdomg  9624  rankr1ai  9838  cofsmo  10309  cfcoflem  10312  inar1  10815  nqerf  10970  prlem936  11087  fimaxre  12212  fiminre  12215  arch  12523  bndndx  12525  suprfinzcl  12732  zmin  12986  elpq  13017  qbtwnxr  13242  qsqueeze  13243  qextltlem  13244  xrsupsslem  13349  xrinfmsslem  13350  xrub  13354  supxrunb1  13361  ssnn0fi  14026  fsuppmapnn0fiub0  14034  fsuppmapnn0fz  14037  expnlbnd2  14273  r19.29uz  15389  cau3lem  15393  rlim2lt  15533  rlimclim  15582  2clim  15608  o1co  15622  climcn1  15628  climcn2  15629  rlimo1  15653  climsqz  15677  climsqz2  15678  rlimsqzlem  15685  lo1le  15688  climsup  15706  climcau  15707  caucvgrlem2  15711  iseralt  15721  cvgcmp  15852  cvgcmpce  15854  supcvg  15892  rpnnen2lem12  16261  bezoutlem1  16576  divgcdcoprmex  16703  exprmfct  16741  prmdvdsfz  16742  prmdvdsncoprmbd  16764  pclem  16876  pc2dvds  16917  pcprmpw  16921  dvdsprmpweqle  16924  unbenlem  16946  infpnlem2  16949  infpn2  16951  prmunb  16952  vdwlem2  17020  ramub1lem2  17065  prmdvdsprmop  17081  prmgaplem7  17095  ipodrsima  18586  smndex1mgm  18920  grpinveu  18992  dfgrp3lem  19056  psgneu  19524  odbezout  19576  sylow2blem3  19640  nn0gsumfz  20002  irredrmul  20427  zrninitoringc  20676  lbsextlem2  21161  znunit  21582  mptcoe1fsupp  22217  evls1fpws  22373  scmate  22516  scmatscm  22519  scmatfo  22536  mat1scmat  22545  pmatcoe1fsupp  22707  pmatcollpwfi  22788  pmatcollpw3fi  22791  mptcoe1matfsupp  22808  pm2mp  22831  chmaidscmat  22854  cpmadumatpoly  22889  chcoeffeq  22892  cayhamlem3  22893  cayhamlem4  22894  neiptopnei  23140  neitr  23188  cnpnei  23272  haust1  23360  isnrm3  23367  isreg2  23385  tgcmp  23409  hauscmplem  23414  hauscmp  23415  bwth  23418  1stcfb  23453  1stcelcls  23469  lly1stc  23504  txcmplem1  23649  txlm  23656  xkococnlem  23667  filuni  23893  filufint  23928  ufilen  23938  fclscf  24033  cnextcn  24075  ustex2sym  24225  ustex3sym  24226  utopreg  24261  isucn2  24288  ucnima  24290  ucncn  24294  neipcfilu  24305  metequiv2  24523  metrest  24537  xrsmopn  24834  mulc1cncf  24931  cncfco  24933  bndth  24990  lmmcvg  25295  cfil3i  25303  iscau4  25313  cmetcaulem  25322  iscmet3lem1  25325  caussi  25331  equivcfil  25333  equivcau  25334  caubl  25342  minveclem3b  25462  ovolgelb  25515  ovollb2lem  25523  ovolctb  25525  ovolicc2lem4  25555  ioombl1lem4  25596  dyadmax  25633  volsup2  25640  itg2monolem1  25785  c1liplem1  26035  c1lip1  26036  dvivthlem1  26047  lhop1  26053  ftc1a  26078  ftc1lem6  26082  ply1divex  26176  elply2  26235  dgrlem  26268  aacjcl  26369  aalioulem2  26375  aalioulem3  26376  aalioulem4  26377  ulmcaulem  26437  ulmcau  26438  ulmss  26440  mtest  26447  itgulm  26451  reeff1o  26491  efif1olem4  26587  rlimcnp  27008  xrlimcnp  27011  lgamucov  27081  ftalem3  27118  fta  27123  muval1  27176  dvdssqf  27181  mumullem1  27222  lgsqrmod  27396  lgsqrmodndvds  27397  pntlem3  27653  ostth  27683  nosupno  27748  nosupbnd1lem4  27756  noinfno  27763  noinfbnd1lem4  27771  conway  27844  etasslt  27858  znegscl  28378  tgtrisegint  28507  tgbtwndiff  28514  tgcgrxfr  28526  lnext  28575  legov2  28594  legtrd  28597  hlcgrex  28624  colperpexlem3  28740  colperpex  28741  hlpasch  28764  hpgerlem  28773  hpgtr  28776  dfcgra2  28838  acopy  28841  inagswap  28849  inaghl  28853  cgrg3col4  28861  axpasch  28956  wwlksnredwwlkn0  29916  midwwlks2s3  29972  clwwlkn1loopb  30062  2pthfrgrrn2  30302  frgrwopreg1  30337  frgrwopreg2  30338  grpoidinvlem3  30525  grpoideu  30528  grpoinveu  30538  ubthlem1  30889  minvecolem5  30900  htthlem  30936  chscllem2  31657  nmopun  32033  lnconi  32052  rnbra  32126  sumdmdii  32434  cdj3lem2b  32456  foresf1o  32523  acunirnmpt  32669  xrofsup  32771  fprodex01  32827  mndlactfo  33032  mndractfo  33034  isarchi3  33194  erler  33269  isarchiofld  33347  dfufd2lem  33577  constrconj  33786  constrextdg2lem  33789  lmxrge0  33951  lmdvg  33952  esumlub  34061  esumfsup  34071  esumcvg  34087  ftc2re  34613  cusgr3cyclex  35141  cvmliftmolem2  35287  cvmlift2lem12  35319  satfv1  35368  satffunlem1lem2  35408  satffunlem2lem2  35411  satfv0fvfmla0  35418  ellcsrspsn  35646  r1peuqusdeg1  35648  wzel  35825  wsuclem  35826  btwndiff  36028  trisegint  36029  cgrxfr  36056  lineext  36077  segcon2  36106  brsegle2  36110  seglecgr12im  36111  segletr  36115  broutsideof3  36127  opnrebl2  36322  nn0prpw  36324  fin2so  37614  poimirlem27  37654  poimirlem30  37657  poimirlem31  37658  poimir  37660  mblfinlem1  37664  mblfinlem2  37665  mblfinlem3  37666  mblfinlem4  37667  itg2addnclem  37678  ftc1cnnc  37699  ftc1anclem5  37704  sdclem1  37750  geomcau  37766  equivtotbnd  37785  bndss  37793  ismtybndlem  37813  heibor1lem  37816  rrncmslem  37839  rngo2  37914  prtlem15  38876  lsateln0  38996  lsat0cv  39034  eqlkr3  39102  lkrshp  39106  lshpset2N  39120  hlhgt2  39391  hlrelat2  39405  atle  39438  athgt  39458  2dim  39472  1cvratex  39475  ps-2  39480  dalem20  39695  lhpexle1lem  40009  lhpexle1  40010  lhpexle2lem  40011  lhpmcvr5N  40029  lhpmcvr6N  40030  cdleme25a  40355  cdleme29ex  40376  cdlemfnid  40566  cdlemg33b0  40703  cdlemg33a  40708  cdlemg35  40715  cdleml3N  40980  dihlsscpre  41236  dih1dimb2  41243  dihatexv  41340  dvh3dim2  41450  dochkr1  41480  dochkr1OLDN  41481  lcfl8  41504  lcfl8b  41506  lcfrlem5  41548  lcfrlem6  41549  mapdrvallem2  41647  mapdh9a  41791  mapdh9aOLDN  41792  hdmaprnlem3eN  41860  hdmaprnlem16N  41864  mndmolinv  42096  primrootsunit1  42098  flt4lem5elem  42661  flt4lem7  42669  nna4b4nsq  42670  fphpdo  42828  rencldnfilem  42831  irrapxlem2  42834  oasubex  43299  tfsconcatlem  43349  tfsconcatrev  43361  cvgdvgrat  44332  expgrowth  44354  projf1o  45202  ssfiunibd  45321  supxrgere  45344  supxrgelem  45348  suplesup  45350  infrpge  45362  infleinf  45383  supxrunb3  45410  unb2ltle  45426  uzub  45442  cvgcaule  45502  qinioo  45548  qelioo  45559  climinf  45621  mullimc  45631  islptre  45634  limccog  45635  mullimcf  45638  limcrecl  45644  sumnnodd  45645  neglimc  45662  0ellimcdiv  45664  limclner  45666  allbutfifvre  45690  climleltrp  45691  fnlimabslt  45694  climinf2lem  45721  limsuppnflem  45725  limsupvaluz2  45753  supcnvlimsup  45755  limsupgtlem  45792  liminflelimsupuz  45800  liminflimsupclim  45822  limsupub2  45827  xlimpnfxnegmnf  45829  cncfioobd  45912  stoweidlem7  46022  stoweidlem27  46042  stoweidlem39  46054  stoweidlem48  46063  stoweidlem49  46064  stoweidlem60  46075  stoweidlem61  46076  stoweid  46078  dirkercncflem2  46119  fourierdlem20  46142  fourierdlem39  46161  fourierdlem41  46163  fourierdlem48  46169  fourierdlem49  46170  fourierdlem50  46171  fourierdlem64  46185  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem87  46208  fourierdlem103  46224  fourierdlem104  46225  qndenserrnopnlem  46312  sge0ltfirp  46415  sge0gerpmpt  46417  sge0ltfirpmpt2  46441  sge0isum  46442  sge0pnffigtmpt  46455  sge0pnffsumgt  46457  sge0gtfsumgt  46458  sge0uzfsumgt  46459  nnfoctbdjlem  46470  meaiuninclem  46495  meaiuninc3v  46499  omeiunltfirp  46534  carageniuncllem2  46537  hoicvr  46563  volicorescl  46568  hoidmv1le  46609  hoidmvlelem3  46612  hoiqssbllem3  46639  hspmbllem2  46642  iunhoiioolem  46690  vonioo  46697  vonicc  46700  smfaddlem1  46778  smflimlem2  46787  smflimlem3  46788  smfmullem4  46809  fsetsnfo  47065  2reu8i  47125  imasetpreimafvbijlemfo  47392  2pwp1prmfmtno  47577  proththd  47601  sbgoldbwt  47764  sbgoldbst  47765  sbgoldbalt  47768  bgoldbtbndlem4  47795  bgoldbtbnd  47796  grtriprop  47908  ply1mulgsumlem3  48305  ply1mulgsumlem4  48306  islindeps2  48400  isldepslvec2  48402