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

Theorem ralimdv 2946
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1729). (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 480 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32ralimdva 2945 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977  wral 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827
This theorem depends on definitions:  df-bi 196  df-an 385  df-ral 2901
This theorem is referenced by:  poss  4961  sess1  5006  sess2  5007  riinint  5303  iinpreima  6253  dffo4  6283  dffo5  6284  isoini2  6489  tfindsg  6952  el2mpt2csbcl  7137  iiner  7706  xpf1o  8007  dffi3  8220  brwdom3  8370  xpwdomg  8373  bndrank  8587  cfub  8954  cff1  8963  cfflb  8964  cfslb2n  8973  cofsmo  8974  cfcoflem  8977  pwcfsdom  9284  fpwwe2lem13  9343  inawinalem  9390  grupr  9498  fsequb  12636  cau3lem  13942  caubnd2  13945  caubnd  13946  rlim2lt  14076  rlim3  14077  climshftlem  14153  isercolllem1  14243  climcau  14249  caucvgb  14258  serf0  14259  modfsummods  14366  cvgcmp  14389  mreriincl  16081  acsfn1c  16146  islss4  18783  riinopn  20538  fiinbas  20567  baspartn  20569  isclo2  20702  lmcls  20916  lmcnp  20918  isnrm3  20973  1stcelcls  21074  llyss  21092  nllyss  21093  ptpjpre1  21184  txlly  21249  txnlly  21250  tx1stc  21263  xkococnlem  21272  fbunfip  21483  filssufilg  21525  cnpflf2  21614  fcfnei  21649  isucn2  21893  rescncf  22508  lebnum  22571  cfilss  22876  fgcfil  22877  iscau4  22885  cmetcaulem  22894  cfilres  22902  caussi  22903  ovolunlem1  23072  ulmclm  23945  ulmcaulem  23952  ulmcau  23953  ulmss  23955  rlimcnp  24492  cxploglim  24504  lgsdchr  24880  pntlemp  25099  axcontlem4  25647  usg2wlkeq  26236  3cyclfrgrarn2  26541  nmlnoubi  27035  lnon0  27037  disjpreima  28779  resspos  28990  resstos  28991  submarchi  29071  crefss  29244  iccllyscon  30486  cvmlift2lem1  30538  ss2mcls  30719  mclsax  30720  poimirlem25  32604  poimirlem27  32606  upixp  32694  caushft  32727  sstotbnd3  32745  totbndss  32746  unichnidl  33000  ispridl2  33007  elrfirn2  36277  mzpsubst  36329  eluzrabdioph  36388  neik0pk1imk0  37365  fourierdlem103  39102  fourierdlem104  39103  qndenserrnbllem  39190  ralralimp  40309  ewlkle  40807  uspgr2wlkeq  40854  umgr1wlknloop  40857  1wlkiswwlksupgr2  41074  3cyclfrgrrn2  41457
  Copyright terms: Public domain W3C validator