Theorem reximdva 3176

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3088

This theorem is used by:  reximddv  3179  reximdvva  3211  reximddv2  3222  wereu2  5648  frpomin  6336  dffo4  7095  nnaordex  8631  frfi  9260  fisupg  9263  marypha1  9410  fiinfg  9477  wemapsolem  9528  unwdomg  9562  rankr1ai  9788  cofsmo  10328  cfcoflem  10331  inar1  10841  nqerf  10996  prlem936  11113  fimaxre  12242  fiminre  12245  arch  12584  bndndx  12586  suprfinzcl  12794  zmin  13052  elpq  13084  qbtwnxr  13311  qsqueeze  13312  qextltlem  13313  xrsupsslem  13418  xrinfmsslem  13419  xrub  13423  supxrunb1  13430  ssnn0fi  14108  fsuppmapnn0fiub0  14116  fsuppmapnn0fz  14119  expnlbnd2  14358  r19.29uz  15498  cau3lem  15502  rlim2lt  15644  rlimclim  15693  2clim  15719  o1co  15733  climcn1  15739  climcn2  15740  rlimo1  15764  climsqz  15788  climsqz2  15789  rlimsqzlem  15796  lo1le  15799  climsup  15817  climcau  15818  caucvgrlem2  15822  iseralt  15832  cvgcmp  15963  cvgcmpce  15965  supcvg  16005  rpnnen2lem12  16373  bezoutlem1  16692  divgcdcoprmex  16821  exprmfct  16860  prmdvdsfz  16861  prmdvdsncoprmbd  16883  pclem  16996  pc2dvds  17037  pcprmpw  17041  dvdsprmpweqle  17044  unbenlem  17066  infpnlem2  17069  infpn2  17071  prmunb  17072  vdwlem2  17140  ramub1lem2  17185  prmdvdsprmop  17201  prmgaplem7  17215  ipodrsima  18695  smndex1mgm  19086  grpinveu  19165  dfgrp3lem  19228  psgneu  19700  odbezout  19752  sylow2blem3  19816  nn0gsumfz  20178  irredrmul  20637  zrninitoringc  20908  lbsextlem2  21417  znunit  21849  mptcoe1fsupp  22513  evls1fpws  22667  scmate  22805  scmatscm  22808  scmatfo  22825  mat1scmat  22834  pmatcoe1fsupp  22999  pmatcollpwfi  23080  pmatcollpw3fi  23083  mptcoe1matfsupp  23100  pm2mp  23123  chmaidscmat  23146  cpmadumatpoly  23181  chcoeffeq  23184  cayhamlem3  23185  cayhamlem4  23186  neiptopnei  23430  neitr  23478  cnpnei  23562  haust1  23650  isnrm3  23657  isreg2  23675  tgcmp  23699  hauscmplem  23704  hauscmp  23705  bwth  23708  1stcfb  23743  1stcelcls  23760  lly1stc  23795  txcmplem1  23940  txlm  23947  xkococnlem  23958  filuni  24184  filufint  24219  ufilen  24229  fclscf  24324  cnextcn  24366  ustex2sym  24516  ustex3sym  24517  utopreg  24551  isucn2  24577  ucnima  24579  ucncn  24583  neipcfilu  24594  metequiv2  24809  metrest  24823  xrsmopn  25112  mulc1cncf  25206  cncfco  25208  bndth  25259  lmmcvg  25562  cfil3i  25570  iscau4  25580  cmetcaulem  25589  iscmet3lem1  25592  caussi  25598  equivcfil  25600  equivcau  25601  caubl  25609  minveclem3b  25729  ovolgelb  25781  ovollb2lem  25789  ovolctb  25791  ovolicc2lem4  25821  ioombl1lem4  25862  dyadmax  25899  volsup2  25906  itg2monolem1  26051  c1liplem1  26296  c1lip1  26297  dvivthlem1  26308  lhop1  26314  ftc1a  26337  ftc1lem6  26341  ply1divex  26435  elply2  26494  dgrlem  26528  aacjcl  26636  aalioulem2  26642  aalioulem3  26643  aalioulem4  26644  ulmcaulem  26703  ulmcau  26704  ulmss  26706  mtest  26713  itgulm  26717  reeff1o  26756  efif1olem4  26855  rlimcnp  27275  xrlimcnp  27278  lgamucov  27347  ftalem3  27384  fta  27389  muval1  27442  dvdssqf  27447  mumullem1  27488  lgsqrmod  27661  lgsqrmodndvds  27662  pntlem3  27918  ostth  27948  flt4lem5elem  27963  flt4lem7  27971  nna4b4nsq  27972  fltoprmlem1  27975  nosupno  28042  nosupbnd1lem4  28050  noinfno  28057  noinfbnd1lem4  28065  conway  28147  etaslts  28161  znegscl  28760  tgtrisegint  28944  tgbtwndiff  28951  tgcgrxfr  28963  lnext  29012  legov2  29031  legtrd  29034  hlcgrex  29064  colperpexlem3  29190  colperpex  29191  hlpasch  29216  hpgerlem  29225  hpgtr  29228  dfcgra2  29320  acopy  29323  inagswap  29342  inaghl  29346  cgrg3col4  29354  axpasch  29501  wwlksnredwwlkn0  30467  midwwlks2s3  30523  clwwlkn1loopb  30616  2pthfrgrrn2  30866  frgrwopreg1  30901  frgrwopreg2  30902  grpoidinvlem3  31090  grpoideu  31093  grpoinveu  31103  ubthlem1  31454  minvecolem5  31465  htthlem  31501  chscllem2  32222  nmopun  32598  lnconi  32617  rnbra  32691  sumdmdii  32999  cdj3lem2b  33021  foresf1o  33082  acunirnmpt  33235  xrofsup  33341  fprodex01  33398  mndlactfo  33570  mndractfo  33572  isarchi3  33730  isarchiofld  33742  erler  33808  erld2  33809  dfufd2lem  34063  constrconj  34359  constrextdg2lem  34362  constrcjcl  34382  lmxrge0  34566  lmdvg  34567  esumlub  34674  esumfsup  34684  esumcvg  34700  ftc2re  35210  cusgr3cyclex  35880  cvmliftmolem2  36016  cvmlift2lem12  36048  satfv1  36097  satffunlem1lem2  36137  satffunlem2lem2  36140  satfv0fvfmla0  36147  ellcsrspsn  36375  r1peuqusdeg1  36377  wzel  36556  wsuclem  36557  btwndiff  36762  trisegint  36763  cgrxfr  36790  lineext  36811  segcon2  36840  brsegle2  36844  seglecgr12im  36845  segletr  36849  broutsideof3  36861  opnrebl2  37079  nn0prpw  37081  fin2so  38498  poimirlem27  38533  poimirlem30  38536  poimirlem31  38537  poimir  38539  mblfinlem1  38543  mblfinlem2  38544  mblfinlem3  38545  mblfinlem4  38546  itg2addnclem  38557  ftc1cnnc  38578  ftc1anclem5  38583  sdclem1  38645  geomcau  38661  equivtotbnd  38680  bndss  38688  ismtybndlem  38708  heibor1lem  38711  rrncmslem  38734  rngo2  38809  prtlem15  39900  lsateln0  40020  lsat0cv  40058  eqlkr3  40126  lkrshp  40130  lshpset2N  40144  hlhgt2  40414  hlrelat2  40428  atle  40461  athgt  40481  2dim  40495  1cvratex  40498  ps-2  40503  dalem20  40718  lhpexle1lem  41032  lhpexle1  41033  lhpexle2lem  41034  lhpmcvr5N  41052  lhpmcvr6N  41053  cdleme25a  41378  cdleme29ex  41399  cdlemfnid  41589  cdlemg33b0  41726  cdlemg33a  41731  cdlemg35  41738  cdleml3N  42003  dihlsscpre  42259  dih1dimb2  42266  dihatexv  42363  dvh3dim2  42473  dochkr1  42503  dochkr1OLDN  42504  lcfl8  42527  lcfl8b  42529  lcfrlem5  42571  lcfrlem6  42572  mapdrvallem2  42670  mapdh9a  42814  mapdh9aOLDN  42815  hdmaprnlem3eN  42883  hdmaprnlem16N  42887  mndmolinv  43113  primrootsunit1  43115  fphpdo  43777  rencldnfilem  43780  irrapxlem2  43783  oasubex  44246  tfsconcatlem  44296  tfsconcatrev  44308  cvgdvgrat  45256  expgrowth  45278  projf1o  46154  ssfiunibd  46268  supxrgere  46289  supxrgelem  46293  suplesup  46295  infrpge  46307  infleinf  46327  supxrunb3  46354  unb2ltle  46369  uzub  46385  cvgcaule  46445  qinioo  46491  qelioo  46502  climinf  46562  mullimc  46572  islptre  46575  limccog  46576  mullimcf  46579  limcrecl  46585  sumnnodd  46586  neglimc  46601  0ellimcdiv  46603  limclner  46605  allbutfifvre  46629  climleltrp  46630  fnlimabslt  46633  climinf2lem  46660  limsuppnflem  46664  limsupvaluz2  46692  supcnvlimsup  46694  limsupgtlem  46731  liminflelimsupuz  46739  liminflimsupclim  46761  limsupub2  46766  xlimpnfxnegmnf  46768  cncfioobd  46851  stoweidlem7  46961  stoweidlem27  46981  stoweidlem39  46993  stoweidlem48  47002  stoweidlem49  47003  stoweidlem60  47014  stoweidlem61  47015  stoweid  47017  dirkercncflem2  47058  fourierdlem20  47081  fourierdlem39  47100  fourierdlem41  47102  fourierdlem48  47108  fourierdlem49  47109  fourierdlem50  47110  fourierdlem64  47124  fourierdlem73  47133  fourierdlem74  47134  fourierdlem75  47135  fourierdlem87  47147  fourierdlem103  47163  fourierdlem104  47164  qndenserrnopnlem  47251  sge0ltfirp  47354  sge0gerpmpt  47356  sge0ltfirpmpt2  47380  sge0isum  47381  sge0pnffigtmpt  47394  sge0pnffsumgt  47396  sge0gtfsumgt  47397  sge0uzfsumgt  47398  nnfoctbdjlem  47409  meaiuninclem  47434  meaiuninc3v  47438  omeiunltfirp  47473  carageniuncllem2  47476  volicorescl  47507  hoidmv1le  47548  hoidmvlelem3  47551  hoiqssbllem3  47578  hspmbllem2  47581  iunhoiioolem  47629  vonioo  47636  vonicc  47639  smfaddlem1  47717  smflimlem2  47726  smflimlem3  47727  smfmullem4  47748  fsetsnfo  48067  2reu8i  48127  imasetpreimafvbijlemfo  48431  2pwp1prmfmtno  48619  proththd  48643  sbgoldbwt  48819  sbgoldbst  48820  sbgoldbalt  48823  bgoldbtbndlem4  48850  bgoldbtbnd  48851  grtriprop  48983  ply1mulgsumlem3  49444  ply1mulgsumlem4  49445  islindeps2  49539  isldepslvec2  49541