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

Theorem ralimdv 3110
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1905). (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 472 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32ralimdva 3109 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2155  wral 3055
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005
This theorem depends on definitions:  df-bi 198  df-an 385  df-ral 3060
This theorem is referenced by:  poss  5200  sess1  5245  sess2  5246  riinint  5551  iinpreima  6535  dffo4  6565  dffo5  6566  isoini2  6781  tfindsg  7258  el2mpt2csbcl  7451  iiner  8022  xpf1o  8329  dffi3  8544  brwdom3  8694  xpwdomg  8697  bndrank  8919  cfub  9324  cff1  9333  cfflb  9334  cfslb2n  9343  cofsmo  9344  cfcoflem  9347  pwcfsdom  9658  fpwwe2lem13  9717  inawinalem  9764  grupr  9872  fsequb  12982  cau3lem  14379  caubnd2  14382  caubnd  14383  rlim2lt  14513  rlim3  14514  climshftlem  14590  isercolllem1  14680  climcau  14686  caucvgb  14695  serf0  14696  modfsummods  14809  cvgcmp  14832  mreriincl  16524  acsfn1c  16588  islss4  19234  riinopn  20992  fiinbas  21036  baspartn  21038  isclo2  21172  lmcls  21386  lmcnp  21388  isnrm3  21443  1stcelcls  21544  llyss  21562  nllyss  21563  ptpjpre1  21654  txlly  21719  txnlly  21720  tx1stc  21733  xkococnlem  21742  fbunfip  21952  filssufilg  21994  cnpflf2  22083  fcfnei  22118  isucn2  22362  rescncf  22979  lebnum  23042  cfilss  23347  fgcfil  23348  iscau4  23356  cmetcaulem  23365  cfilres  23373  caussi  23374  ovolunlem1  23555  ulmclm  24432  ulmcaulem  24439  ulmcau  24440  ulmss  24442  rlimcnp  24983  cxploglim  24995  lgsdchr  25371  pntlemp  25590  axcontlem4  26138  ewlkle  26792  uspgr2wlkeq  26833  umgrwlknloop  26836  wlkiswwlksupgr2  27068  3cyclfrgrrn2  27567  nmlnoubi  28107  lnon0  28109  disjpreima  29845  resspos  30106  resstos  30107  submarchi  30187  crefss  30363  iccllysconn  31680  cvmlift2lem1  31732  ss2mcls  31913  mclsax  31914  nosupno  32293  nosupres  32297  sssslt2  32351  poimirlem25  33858  poimirlem27  33860  upixp  33947  caushft  33979  sstotbnd3  33997  totbndss  33998  unichnidl  34252  ispridl2  34259  elrfirn2  37937  mzpsubst  37989  eluzrabdioph  38048  neik0pk1imk0  39019  limsupub  40574  limsupre3lem  40602  climuzlem  40613  xlimbr  40691  fourierdlem103  41063  fourierdlem104  41064  qndenserrnbllem  41151  ralralimp  42027
  Copyright terms: Public domain W3C validator