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

Theorem ralimdv 2945
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1728). (Contributed by NM, 8-Oct-2003.)
Hypothesis
Ref Expression
ralimdv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
ralimdv (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralimdv
StepHypRef Expression
1 ralimdv.1 . . 3 (𝜑 → (𝜓𝜒))
21adantr 479 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32ralimdva 2944 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  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:  poss  4951  sess1  4996  sess2  4997  riinint  5290  iinpreima  6238  dffo4  6268  dffo5  6269  isoini2  6467  tfindsg  6929  el2mpt2csbcl  7114  iiner  7683  xpf1o  7984  dffi3  8197  brwdom3  8347  xpwdomg  8350  bndrank  8564  cfub  8931  cff1  8940  cfflb  8941  cfslb2n  8950  cofsmo  8951  cfcoflem  8954  pwcfsdom  9261  fpwwe2lem13  9320  inawinalem  9367  grupr  9475  fsequb  12591  cau3lem  13888  caubnd2  13891  caubnd  13892  rlim2lt  14022  rlim3  14023  climshftlem  14099  isercolllem1  14189  climcau  14195  caucvgb  14204  serf0  14205  modfsummods  14312  cvgcmp  14335  mreriincl  16027  acsfn1c  16092  islss4  18729  riinopn  20480  fiinbas  20509  baspartn  20511  isclo2  20644  lmcls  20858  lmcnp  20860  isnrm3  20915  1stcelcls  21016  llyss  21034  nllyss  21035  ptpjpre1  21126  txlly  21191  txnlly  21192  tx1stc  21205  xkococnlem  21214  fbunfip  21425  filssufilg  21467  cnpflf2  21556  fcfnei  21591  isucn2  21835  rescncf  22439  lebnum  22502  cfilss  22794  fgcfil  22795  iscau4  22803  cmetcaulem  22812  cfilres  22820  caussi  22821  ovolunlem1  22989  ulmclm  23862  ulmcaulem  23869  ulmcau  23870  ulmss  23872  rlimcnp  24409  cxploglim  24421  lgsdchr  24797  pntlemp  25016  axcontlem4  25565  usg2wlkeq  26002  3cyclfrgrarn2  26307  nmlnoubi  26841  lnon0  26843  disjpreima  28585  resspos  28796  resstos  28797  submarchi  28877  crefss  29050  iccllyscon  30292  cvmlift2lem1  30344  ss2mcls  30525  mclsax  30526  poimirlem25  32407  poimirlem27  32409  upixp  32497  caushft  32530  sstotbnd3  32548  totbndss  32549  unichnidl  32803  ispridl2  32810  elrfirn2  36080  mzpsubst  36132  eluzrabdioph  36191  neik0pk1imk0  37168  fourierdlem103  38906  fourierdlem104  38907  qndenserrnbllem  38994  ralralimp  40114  ewlkle  40809  uspgr2wlkeq  40856  umgr1wlknloop  40859  1wlkiswwlksupgr2  41076  3cyclfrgrrn2  41459
  Copyright terms: Public domain W3C validator