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

Theorem ralimdva 3147
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 416 . . 3 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32a2d 29 . 2 (𝜑 → ((𝑥𝐴𝜓) → (𝑥𝐴𝜒)))
43ralimdv2 3146 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2112  wral 3109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911
This theorem depends on definitions:  df-bi 210  df-an 400  df-ral 3114
This theorem is referenced by:  ralimdv  3148  ralimdvva  3149  wereu2  5520  fveqressseq  6828  f1mpt  7001  isores3  7071  caofrss  7426  caoftrn  7428  sorpssuni  7442  sorpssint  7443  onint  7494  smogt  7991  fisupg  8754  ixpfi2  8810  fissuni  8817  indexfi  8820  fiinfg  8951  wemaplem2  8999  rankonidlem  9245  ac5num  9451  acni2  9461  acndom2  9469  alephle  9503  dfac5  9543  cfsmolem  9685  isf34lem7  9794  isf34lem6  9795  fin1a2s  9829  acncc  9855  ttukeylem6  9929  fpwwe2lem8  10052  gchina  10114  inar1  10190  tskord  10195  grudomon  10232  grur1a  10234  dedekind  10796  fimaxre  11577  fiminre  11580  uzwo  12303  xrsupsslem  12692  xrinfmsslem  12693  fsuppmapnn0fiub0  13360  rexanre  14702  rexuz3  14704  rexico  14709  cau3lem  14710  limsupval2  14833  rlim2lt  14850  rlim3  14851  lo1bdd2  14877  lo1bddrp  14878  o1lo1  14890  climrlim2  14900  2clim  14925  o1co  14939  rlimcn1  14941  rlimcn2  14943  climcn1  14944  climcn2  14945  subcn2  14947  o1of2  14965  rlimo1  14969  o1rlimmul  14971  lo1add  14979  lo1mul  14980  climsqz  14993  climsqz2  14994  rlimsqzlem  15001  lo1le  15004  climbdd  15024  caucvgrlem  15025  caucvgrlem2  15027  caurcvg2  15030  iseralt  15037  cvgcmp  15167  cvgcmpce  15169  gcdcllem1  15842  absproddvds  15955  coprmprod  15999  coprmproddvdslem  16000  pcfac  16229  pockthg  16236  infpnlem1  16240  prmreclem2  16247  prmreclem3  16248  vdwlem11  16321  vdwlem13  16323  vdwnnlem3  16327  isacs2  16920  acsfn1  16928  acsfn2  16930  catpropd  16975  drsdirfi  17544  ipodrsima  17771  isacs5  17778  mrelatglb  17790  mrelatlub  17792  isgrpinv  18152  dfgrp3e  18195  issubg4  18294  gsmsymgreqlem2  18555  gexdvds  18705  gexcl3  18708  sylow2blem3  18743  cyggeninv  18999  gsummptnn0fz  19103  dprdff  19131  issubdrg  19557  acsfn1p  19575  cygznlem3  20265  mptcoe1fsupp  20848  cply1coe0bi  20933  gsummoncoe1  20937  scmatdmat  21124  mdetdiagid  21209  mdetunilem9  21229  cpmatmcllem  21327  m2cpminvid2lem  21363  decpmatmulsumfsupp  21382  pmatcollpw1lem1  21383  pmatcollpw2lem  21386  pmatcollpwfi  21391  pm2mpf1  21408  mptcoe1matfsupp  21411  mp2pm2mplem4  21418  pm2mpmhmlem1  21427  pm2mp  21434  chpdmat  21450  chpscmat  21451  cpmidpmatlem3  21481  cayhamlem4  21497  neiptopnei  21741  cncnp  21889  isnrm2  21967  isreg2  21986  2ndcdisj  22065  islly2  22093  dislly  22106  kgen2ss  22164  ptbasfi  22190  ptclsg  22224  prdstopn  22237  txtube  22249  txlm  22257  isr0  22346  filuni  22494  alexsubALTlem3  22658  ptcmplem3  22663  ptcmplem4  22664  tsmsxplem1  22762  prdsmet  22981  metequiv2  23121  metcnpi3  23157  nmoleub  23341  rescncf  23506  cncfco  23516  evth  23568  lebnumlem3  23572  xlebnum  23574  nmoleub2lem2  23725  nmhmcn  23729  lmmcvg  23869  cmetcaulem  23896  caubl  23916  bcth3  23939  ovollb2lem  24096  ovoliunlem2  24111  ovolicc2lem3  24127  ovolicc2lem4  24128  nulmbl2  24144  volsup  24164  ioombl1lem4  24169  dyadmax  24206  vitalilem2  24217  vitalilem5  24220  mbfi1flimlem  24330  itg2seq  24350  itg2addlem  24366  itgcn  24452  limciun  24501  rolle  24597  dvfsumrlim  24638  itgsubst  24656  aannenlem1  24928  aalioulem3  24934  ulmcaulem  24993  ulmcau  24994  ulmss  24996  ulmbdd  24997  ulmcn  24998  ulmdvlem3  25001  mtest  25003  iblulm  25006  itgulm  25007  rlimcnp  25555  xrlimcnp  25558  rlimcxp  25563  o1cxp  25564  amgm  25580  lgambdd  25626  ftalem2  25663  isppw2  25704  mumullem2  25769  2sqlem6  26011  chtppilimlem2  26062  chtppilim  26063  pntrsumbnd2  26155  pntlem3  26197  isperp2  26513  axeuclidlem  26760  axeuclid  26761  uhgrnbgr0nb  27148  vtxdginducedm1fi  27338  cusgrrusgr  27375  rusgrpropnb  27377  rusgrpropedg  27378  rusgrpropadjvtx  27379  upgrewlkle2  27400  wlkvtxiedg  27418  upgrwlkvtxedg  27438  uspgr2wlkeq  27439  redwlk  27466  wlkdlem2  27477  lfgrwlkprop  27481  2pthnloop  27524  upgr2pthnlp  27525  pthdlem1  27559  pthdlem2lem  27560  wlkiswwlks1  27657  wlkiswwlks2lem4  27662  wwlksm1edg  27671  wwlksnred  27682  clwwlkccatlem  27778  clwlkclwwlklem2a  27787  clwlkclwwlklem2  27789  cusconngr  27980  eucrctshift  28032  2pthfrgr  28073  3cyclfrgr  28077  nmoub3i  28560  ubthlem1  28657  ubthlem3  28659  ocsh  29070  chintcli  29118  chscllem2  29425  nmopub2tALT  29696  nmfnleub2  29713  lnconi  29820  riesz1  29852  rnbra  29894  leopadd  29919  leopmuli  29920  leoptr  29924  dmdbr3  30092  dmdbr4  30093  dmdbr5  30095  mdsl0  30097  mdsymlem6  30195  cdj1i  30220  acunirnmpt  30426  xrge0infss  30514  elrspunidl  31018  cmppcmp  31215  zarclsiin  31228  lmxrge0  31309  ftc2re  31983  cvmlift2lem12  32675  frpomin  33192  nosupbnd1lem5  33326  noetalem3  33333  opnrebl2  33783  neibastop1  33821  neibastop2lem  33822  neibastop3  33824  finixpnum  35041  lindsenlbs  35051  matunitlindflem1  35052  matunitlindflem2  35053  ptrecube  35056  poimirlem26  35082  poimirlem27  35083  poimirlem29  35085  poimirlem30  35086  poimir  35089  heicant  35091  itg2addnclem  35107  itg2addnclem3  35109  itg2addnc  35110  filbcmb  35177  nninfnub  35188  geomcau  35196  sstotbnd2  35211  isbndx  35219  prdsbnd  35230  heibor1lem  35246  heiborlem1  35248  heibor  35258  rrncmslem  35269  intidl  35466  pclclN  37186  lauteq  37390  ltrnid  37430  mapdh9a  39084  elrfirn2  39634  isnacs3  39648  rencldnfilem  39758  kelac1  40004  neik0pk1imk0  40747  cvgdvgrat  41014  neglimc  42286  limsupub  42343  limsuppnflem  42349  limsupre3lem  42371  limsupvaluz2  42377  supcnvlimsup  42379  climuzlem  42382  liminfval2  42407  limsupgtlem  42416  liminflelimsupuz  42424  liminflimsupclim  42446  xlimpnfxnegmnf  42453  liminflimsupxrre  42456  xlimmnfv  42473  xlimpnfv  42477  stoweidlem7  42646  fourierdlem73  42818  sge0isum  43063  meaiuninc3v  43120  preimageiingt  43352  preimaleiinlt  43353  smflimlem3  43403  smflimlem4  43404  2reu8i  43666  iccpartres  43932  upwlkwlk  44364  upgrwlkupwlk  44365  copisnmnd  44426  2zrngnmlid2  44572  ply1mulgsumlem1  44791  ply1mulgsumlem3  44793  ply1mulgsumlem4  44794  snlindsntor  44877  eenglngeehlnmlem1  45148  eenglngeehlnmlem2  45149
  Copyright terms: Public domain W3C validator