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

Theorem ralim 2932
 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 2931 1 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀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 This theorem depends on definitions:  df-bi 196  df-ral 2901 This theorem is referenced by:  ralimdaa  2941  r19.30  3063  trint  4696  mpteqb  6207  tz7.49  7427  mptelixpg  7831  resixpfo  7832  bnd  8638  kmlem12  8866  lbzbi  11652  r19.29uz  13938  caubnd  13946  alzdvds  14880  ptclsg  21228  isucn2  21893  usgreghash2spot  26596  omssubadd  29689  dfon2lem8  30939  dford3lem2  36612  neik0pk1imk0  37365  fusgreghash2wsp  41502
 Copyright terms: Public domain W3C validator