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

Theorem ralimdva 2944
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 448 . . 3 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32a2d 29 . 2 (𝜑 → ((𝑥𝐴𝜓) → (𝑥𝐴𝜒)))
43ralimdv2 2943 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 1976  wral 2895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826
This theorem depends on definitions:  df-bi 195  df-an 384  df-ral 2900
This theorem is referenced by:  ralimdv  2945  ralimdvva  2946  wereu2  5025  fveqressseq  6248  f1mpt  6397  isores3  6463  caofrss  6806  caoftrn  6808  sorpssuni  6822  sorpssint  6823  onint  6865  smogt  7329  fisupg  8071  ixpfi2  8125  fissuni  8132  indexfi  8135  fiinfg  8266  wemaplem2  8313  rankonidlem  8552  ac5num  8720  acni2  8730  acndom2  8738  alephle  8772  dfac5  8812  cfsmolem  8953  isf34lem7  9062  isf34lem6  9063  fin1a2s  9097  acncc  9123  ttukeylem6  9197  fpwwe2lem8  9316  gchina  9378  inar1  9454  tskord  9459  grudomon  9496  grur1a  9498  dedekind  10052  fimaxre  10820  uzwo  11586  xrsupsslem  11968  xrinfmsslem  11969  fsuppmapnn0fiub0  12613  rexanre  13883  rexuz3  13885  rexico  13890  cau3lem  13891  limsupval2  14008  rlim2lt  14025  rlim3  14026  lo1bdd2  14052  lo1bddrp  14053  o1lo1  14065  climrlim2  14075  2clim  14100  o1co  14114  rlimcn1  14116  rlimcn2  14118  climcn1  14119  climcn2  14120  subcn2  14122  o1of2  14140  rlimo1  14144  o1rlimmul  14146  lo1add  14154  lo1mul  14155  climsqz  14168  climsqz2  14169  rlimsqzlem  14176  lo1le  14179  climbdd  14199  caucvgrlem  14200  caucvgrlem2  14202  caurcvg2  14205  iseralt  14212  cvgcmp  14338  cvgcmpce  14340  gcdcllem1  15008  absproddvds  15117  coprmprod  15162  coprmproddvdslem  15163  pcfac  15390  pockthg  15397  infpnlem1  15401  prmreclem2  15408  prmreclem3  15409  vdwlem11  15482  vdwlem13  15484  vdwnnlem3  15488  isacs2  16086  acsfn1  16094  acsfn2  16096  catpropd  16141  drsdirfi  16710  ipodrsima  16937  isacs5  16944  mrelatglb  16956  mrelatlub  16958  isgrpinv  17244  dfgrp3e  17287  issubg4  17385  gsmsymgreqlem2  17623  gexdvds  17771  gexcl3  17774  sylow2blem3  17809  cyggeninv  18057  gsummptnn0fz  18154  dprdff  18183  issubdrg  18577  mptcoe1fsupp  19355  cply1coe0bi  19440  gsummoncoe1  19444  cygznlem3  19685  scmatdmat  20088  mdetdiagid  20173  mdetunilem9  20193  cpmatmcllem  20290  m2cpminvid2lem  20326  decpmatmulsumfsupp  20345  pmatcollpw1lem1  20346  pmatcollpw2lem  20349  pmatcollpwfi  20354  pm2mpf1  20371  mptcoe1matfsupp  20374  mp2pm2mplem4  20381  pm2mpmhmlem1  20390  pm2mp  20397  chpdmat  20413  chpscmat  20414  cpmidpmatlem3  20444  cayhamlem4  20460  neiptopnei  20694  cncnp  20842  isnrm2  20920  isreg2  20939  2ndcdisj  21017  islly2  21045  dislly  21058  kgen2ss  21116  ptbasfi  21142  ptclsg  21176  prdstopn  21189  txtube  21201  txlm  21209  isr0  21298  filuni  21447  alexsubALTlem3  21611  ptcmplem3  21616  ptcmplem4  21617  tsmsxplem1  21714  prdsmet  21933  metequiv2  22073  metcnpi3  22109  nmoleub  22293  rescncf  22456  cncfco  22466  evth  22514  lebnumlem3  22518  xlebnum  22520  nmoleub2lem2  22672  nmhmcn  22676  lmmcvg  22812  cmetcaulem  22839  caubl  22859  bcth3  22881  ovollb2lem  23008  ovoliunlem2  23023  ovolicc2lem3  23039  ovolicc2lem4  23040  nulmbl2  23056  volsup  23076  ioombl1lem4  23081  dyadmax  23117  vitalilem2  23129  vitalilem5  23132  mbfi1flimlem  23240  itg2seq  23260  itg2addlem  23276  itgcn  23360  limciun  23409  rolle  23502  dvfsumrlim  23543  itgsubst  23561  aannenlem1  23832  aalioulem3  23838  ulmcaulem  23897  ulmcau  23898  ulmss  23900  ulmbdd  23901  ulmcn  23902  ulmdvlem3  23905  mtest  23907  iblulm  23910  itgulm  23911  rlimcnp  24437  xrlimcnp  24440  rlimcxp  24445  o1cxp  24446  amgm  24462  lgambdd  24508  ftalem2  24545  isppw2  24586  mumullem2  24651  2sqlem6  24893  chtppilimlem2  24908  chtppilim  24909  pntrsumbnd2  25001  pntlem3  25043  isperp2  25356  axeuclidlem  25588  axeuclid  25589  cusgrares  25795  edgwlk  25853  usgrwlknloop  25887  redwlk  25930  cusconngra  25998  wlkiswwlk1  26012  wlkiswwlk2lem4  26016  usg2wlkeq  26030  wwlknred  26045  wwlkm1edg  26057  clwlkisclwwlklem2a  26107  clwlkisclwwlklem1  26109  usgravd00  26240  cusgraisrusgra  26259  rusgraprop2  26263  rusgraprop3  26264  frisusgranb  26318  2pthfrgrarn  26330  2pthfrgrarn2  26331  2pthfrgra  26332  3cyclfrgra  26336  frgrancvvdeq  26363  frgrancvvdgeq  26364  nmoub3i  26846  ubthlem1  26944  ubthlem3  26946  ocsh  27360  chintcli  27408  chscllem2  27715  nmopub2tALT  27986  nmfnleub2  28003  lnconi  28110  riesz1  28142  rnbra  28184  leopadd  28209  leopmuli  28210  leoptr  28214  dmdbr3  28382  dmdbr4  28383  dmdbr5  28385  mdsl0  28387  mdsymlem6  28485  cdj1i  28510  acunirnmpt  28675  xrge0infss  28749  cmppcmp  29087  lmxrge0  29160  cvmlift2lem12  30384  opnrebl2  31320  neibastop1  31358  neibastop2lem  31359  neibastop3  31361  finixpnum  32388  lindsenlbs  32398  matunitlindflem1  32399  matunitlindflem2  32400  ptrecube  32403  poimirlem26  32429  poimirlem27  32430  poimirlem29  32432  poimirlem30  32433  poimir  32436  heicant  32438  itg2addnclem  32455  itg2addnclem3  32457  itg2addnc  32458  filbcmb  32529  nninfnub  32541  geomcau  32549  sstotbnd2  32567  isbndx  32575  prdsbnd  32586  heibor1lem  32602  heiborlem1  32604  heibor  32614  rrncmslem  32625  intidl  32822  pclclN  34019  lauteq  34223  ltrnid  34263  mapdh9a  35921  elrfirn2  36101  isnacs3  36115  rencldnfilem  36226  kelac1  36475  acsfn1p  36612  neik0pk1imk0  37189  cvgdvgrat  37358  neglimc  38538  stoweidlem7  38724  fourierdlem73  38896  sge0isum  39144  preimageiingt  39431  preimaleiinlt  39432  smflimlem3  39483  smflimlem4  39484  iccpartres  39781  uhgrnbgr0nb  40598  cusgrrusgr  40803  rusgrpropnb  40805  rusgrpropedg  40806  rusgrpropadjvtx  40807  upgrewlkle2  40830  1wlkvtxiedg  40851  wlk1wlk  40868  upgr1wlkwlk  40869  upgr1wlkvtxedg  40875  uspgr2wlkeq  40876  red1wlk  40903  1wlkdlem2  40914  lfgrwlkprop  40918  2pthnloop  40959  upgr2pthnlp  40960  pthdlem1  40994  pthdlem2lem  40995  1wlkiswwlks1  41086  1wlkiswwlks2lem4  41091  wwlksm1edg  41100  wwlksnred  41120  clwlkclwwlklem2a  41229  clwlkclwwlklem2  41231  cusconngr  41380  eucrctshift  41433  2pthfrgr  41476  3cyclfrgr  41480  copisnmnd  41621  2zrngnmlid2  41763  ply1mulgsumlem1  41990  ply1mulgsumlem3  41992  ply1mulgsumlem4  41993  snlindsntor  42076
  Copyright terms: Public domain W3C validator