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

Theorem ralimdv 3178
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1807). (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 483 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32ralimdva 3177 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2110  wral 3138
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907
This theorem depends on definitions:  df-bi 209  df-an 399  df-ral 3143
This theorem is referenced by:  ss2ralv  4034  poss  5475  sess1  5522  sess2  5523  riinint  5838  iinpreima  6836  dffo4  6868  dffo5  6869  isoini2  7091  tfindsg  7574  el2mpocsbcl  7779  iiner  8368  xpf1o  8678  dffi3  8894  brwdom3  9045  xpwdomg  9048  bndrank  9269  cfub  9670  cff1  9679  cfflb  9680  cfslb2n  9689  cofsmo  9690  cfcoflem  9693  pwcfsdom  10004  fpwwe2lem13  10063  inawinalem  10110  grupr  10218  fsequb  13342  cau3lem  14713  caubnd2  14716  caubnd  14717  rlim2lt  14853  rlim3  14854  climshftlem  14930  climcau  15026  caucvgb  15035  serf0  15036  modfsummods  15147  cvgcmp  15170  mreriincl  16868  acsfn1c  16932  islss4  19733  riinopn  21515  fiinbas  21559  baspartn  21561  isclo2  21695  lmcls  21909  lmcnp  21911  isnrm3  21966  1stcelcls  22068  llyss  22086  nllyss  22087  ptpjpre1  22178  txlly  22243  txnlly  22244  tx1stc  22257  xkococnlem  22266  fbunfip  22476  filssufilg  22518  cnpflf2  22607  fcfnei  22642  isucn2  22887  rescncf  23504  lebnum  23567  cfilss  23872  fgcfil  23873  iscau4  23881  cmetcaulem  23890  caussi  23899  ovolunlem1  24097  ulmclm  24974  ulmcaulem  24981  ulmcau  24982  ulmss  24984  rlimcnp  25542  cxploglim  25554  2sqreunnlem2  26030  pntlemp  26185  axcontlem4  26752  ewlkle  27386  uspgr2wlkeq  27426  umgrwlknloop  27429  wlkiswwlksupgr2  27654  3cyclfrgrrn2  28065  nmlnoubi  28572  lnon0  28574  disjpreima  30333  resspos  30646  resstos  30647  submarchi  30815  prmidl2  30958  crefss  31113  iccllysconn  32497  cvmlift2lem1  32549  dmopab3rexdif  32652  ss2mcls  32815  mclsax  32816  nosupno  33203  nosupres  33207  sssslt2  33261  isinf2  34685  poimirlem25  34916  poimirlem27  34918  upixp  35003  caushft  35035  sstotbnd3  35053  totbndss  35054  unichnidl  35308  ispridl2  35315  elrfirn2  39293  mzpsubst  39345  eluzrabdioph  39403  neik0pk1imk0  40397  mnuop3d  40607  limsupub  41985  limsupre3lem  42013  climuzlem  42024  xlimbr  42108  fourierdlem103  42495  fourierdlem104  42496  qndenserrnbllem  42580  2reuimp  43315  ralralimp  43478
  Copyright terms: Public domain W3C validator