MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralimdva Structured version   Visualization version   GIF version

Theorem ralimdva 2991
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.)
Hypothesis
Ref Expression
ralimdva.1 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
ralimdva (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralimdva
StepHypRef Expression
1 ralimdva.1 . . . 4 ((𝜑𝑥𝐴) → (𝜓𝜒))
21ex 449 . . 3 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32a2d 29 . 2 (𝜑 → ((𝑥𝐴𝜓) → (𝑥𝐴𝜒)))
43ralimdv2 2990 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-an 385  df-ral 2946
This theorem is referenced by:  ralimdv  2992  ralimdvva  2993  wereu2  5140  fveqressseq  6395  f1mpt  6558  isores3  6625  caofrss  6972  caoftrn  6974  sorpssuni  6988  sorpssint  6989  onint  7037  smogt  7509  fisupg  8249  ixpfi2  8305  fissuni  8312  indexfi  8315  fiinfg  8446  wemaplem2  8493  rankonidlem  8729  ac5num  8897  acni2  8907  acndom2  8915  alephle  8949  dfac5  8989  cfsmolem  9130  isf34lem7  9239  isf34lem6  9240  fin1a2s  9274  acncc  9300  ttukeylem6  9374  fpwwe2lem8  9497  gchina  9559  inar1  9635  tskord  9640  grudomon  9677  grur1a  9679  dedekind  10238  fimaxre  11006  uzwo  11789  xrsupsslem  12175  xrinfmsslem  12176  fsuppmapnn0fiub0  12833  rexanre  14130  rexuz3  14132  rexico  14137  cau3lem  14138  limsupval2  14255  rlim2lt  14272  rlim3  14273  lo1bdd2  14299  lo1bddrp  14300  o1lo1  14312  climrlim2  14322  2clim  14347  o1co  14361  rlimcn1  14363  rlimcn2  14365  climcn1  14366  climcn2  14367  subcn2  14369  o1of2  14387  rlimo1  14391  o1rlimmul  14393  lo1add  14401  lo1mul  14402  climsqz  14415  climsqz2  14416  rlimsqzlem  14423  lo1le  14426  climbdd  14446  caucvgrlem  14447  caucvgrlem2  14449  caurcvg2  14452  iseralt  14459  cvgcmp  14592  cvgcmpce  14594  gcdcllem1  15268  absproddvds  15377  coprmprod  15422  coprmproddvdslem  15423  pcfac  15650  pockthg  15657  infpnlem1  15661  prmreclem2  15668  prmreclem3  15669  vdwlem11  15742  vdwlem13  15744  vdwnnlem3  15748  isacs2  16361  acsfn1  16369  acsfn2  16371  catpropd  16416  drsdirfi  16985  ipodrsima  17212  isacs5  17219  mrelatglb  17231  mrelatlub  17233  isgrpinv  17519  dfgrp3e  17562  issubg4  17660  gsmsymgreqlem2  17897  gexdvds  18045  gexcl3  18048  sylow2blem3  18083  cyggeninv  18331  gsummptnn0fz  18428  dprdff  18457  issubdrg  18853  mptcoe1fsupp  19633  cply1coe0bi  19718  gsummoncoe1  19722  cygznlem3  19966  scmatdmat  20369  mdetdiagid  20454  mdetunilem9  20474  cpmatmcllem  20571  m2cpminvid2lem  20607  decpmatmulsumfsupp  20626  pmatcollpw1lem1  20627  pmatcollpw2lem  20630  pmatcollpwfi  20635  pm2mpf1  20652  mptcoe1matfsupp  20655  mp2pm2mplem4  20662  pm2mpmhmlem1  20671  pm2mp  20678  chpdmat  20694  chpscmat  20695  cpmidpmatlem3  20725  cayhamlem4  20741  neiptopnei  20984  cncnp  21132  isnrm2  21210  isreg2  21229  2ndcdisj  21307  islly2  21335  dislly  21348  kgen2ss  21406  ptbasfi  21432  ptclsg  21466  prdstopn  21479  txtube  21491  txlm  21499  isr0  21588  filuni  21736  alexsubALTlem3  21900  ptcmplem3  21905  ptcmplem4  21906  tsmsxplem1  22003  prdsmet  22222  metequiv2  22362  metcnpi3  22398  nmoleub  22582  rescncf  22747  cncfco  22757  evth  22805  lebnumlem3  22809  xlebnum  22811  nmoleub2lem2  22962  nmhmcn  22966  lmmcvg  23105  cmetcaulem  23132  caubl  23152  bcth3  23174  ovollb2lem  23302  ovoliunlem2  23317  ovolicc2lem3  23333  ovolicc2lem4  23334  nulmbl2  23350  volsup  23370  ioombl1lem4  23375  dyadmax  23412  vitalilem2  23423  vitalilem5  23426  mbfi1flimlem  23534  itg2seq  23554  itg2addlem  23570  itgcn  23654  limciun  23703  rolle  23798  dvfsumrlim  23839  itgsubst  23857  aannenlem1  24128  aalioulem3  24134  ulmcaulem  24193  ulmcau  24194  ulmss  24196  ulmbdd  24197  ulmcn  24198  ulmdvlem3  24201  mtest  24203  iblulm  24206  itgulm  24207  rlimcnp  24737  xrlimcnp  24740  rlimcxp  24745  o1cxp  24746  amgm  24762  lgambdd  24808  ftalem2  24845  isppw2  24886  mumullem2  24951  2sqlem6  25193  chtppilimlem2  25208  chtppilim  25209  pntrsumbnd2  25301  pntlem3  25343  isperp2  25655  axeuclidlem  25887  axeuclid  25888  uhgrnbgr0nb  26295  vtxdginducedm1fi  26496  cusgrrusgr  26533  rusgrpropnb  26535  rusgrpropedg  26536  rusgrpropadjvtx  26537  upgrewlkle2  26558  wlkvtxiedg  26576  upgrwlkvtxedg  26597  uspgr2wlkeq  26598  redwlk  26625  wlkdlem2  26636  lfgrwlkprop  26640  2pthnloop  26683  upgr2pthnlp  26684  pthdlem1  26718  pthdlem2lem  26719  wlkiswwlks1  26821  wlkiswwlks2lem4  26826  wwlksm1edg  26835  wwlksnred  26855  clwlkclwwlklem2a  26964  clwlkclwwlklem2  26966  cusconngr  27169  eucrctshift  27221  2pthfrgr  27264  3cyclfrgr  27268  clwwlkccatlem  27331  nmoub3i  27756  ubthlem1  27854  ubthlem3  27856  ocsh  28270  chintcli  28318  chscllem2  28625  nmopub2tALT  28896  nmfnleub2  28913  lnconi  29020  riesz1  29052  rnbra  29094  leopadd  29119  leopmuli  29120  leoptr  29124  dmdbr3  29292  dmdbr4  29293  dmdbr5  29295  mdsl0  29297  mdsymlem6  29395  cdj1i  29420  acunirnmpt  29587  xrge0infss  29653  cmppcmp  30053  lmxrge0  30126  ftc2re  30804  cvmlift2lem12  31422  frpomin  31863  nosupbnd1lem5  31983  noetalem3  31990  opnrebl2  32441  neibastop1  32479  neibastop2lem  32480  neibastop3  32482  finixpnum  33524  lindsenlbs  33534  matunitlindflem1  33535  matunitlindflem2  33536  ptrecube  33539  poimirlem26  33565  poimirlem27  33566  poimirlem29  33568  poimirlem30  33569  poimir  33572  heicant  33574  itg2addnclem  33591  itg2addnclem3  33593  itg2addnc  33594  filbcmb  33665  nninfnub  33677  geomcau  33685  sstotbnd2  33703  isbndx  33711  prdsbnd  33722  heibor1lem  33738  heiborlem1  33740  heibor  33750  rrncmslem  33761  intidl  33958  pclclN  35495  lauteq  35699  ltrnid  35739  mapdh9a  37396  elrfirn2  37576  isnacs3  37590  rencldnfilem  37701  kelac1  37950  acsfn1p  38086  neik0pk1imk0  38662  cvgdvgrat  38829  neglimc  40197  limsupub  40254  limsuppnflem  40260  limsupre3lem  40282  limsupvaluz2  40288  supcnvlimsup  40290  climuzlem  40293  liminfval2  40318  limsupgtlem  40327  liminflelimsupuz  40335  liminflimsupclim  40357  xlimmnfv  40378  xlimpnfv  40382  stoweidlem7  40542  fourierdlem73  40714  sge0isum  40962  meaiuninc3v  41019  preimageiingt  41251  preimaleiinlt  41252  smflimlem3  41302  smflimlem4  41303  iccpartres  41679  upwlkwlk  42045  upgrwlkupwlk  42046  copisnmnd  42134  2zrngnmlid2  42276  ply1mulgsumlem1  42499  ply1mulgsumlem3  42501  ply1mulgsumlem4  42502  snlindsntor  42585
  Copyright terms: Public domain W3C validator