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

Theorem ralim 2977
 Description: Distribution of restricted quantification over implication. (Contributed by NM, 9-Feb-1997.) (Proof shortened by Wolf Lammen, 1-Dec-2019.)
Assertion
Ref Expression
ralim (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓))

Proof of Theorem ralim
StepHypRef Expression
1 id 22 . 2 ((𝜑𝜓) → (𝜑𝜓))
21ral2imi 2976 1 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wral 2941 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777 This theorem depends on definitions:  df-bi 197  df-ral 2946 This theorem is referenced by:  ralimdaa  2987  r19.30  3111  trint  4801  mpteqb  6338  tz7.49  7585  mptelixpg  7987  resixpfo  7988  bnd  8793  kmlem12  9021  lbzbi  11814  r19.29uz  14134  caubnd  14142  alzdvds  15089  ptclsg  21466  isucn2  22130  fusgreghash2wsp  27318  omssubadd  30490  dfon2lem8  31819  dford3lem2  37911  neik0pk1imk0  38662
 Copyright terms: Public domain W3C validator