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

Theorem ralim 2948
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 2947 1 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wral 2912
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734
This theorem depends on definitions:  df-bi 197  df-ral 2917
This theorem is referenced by:  ralimdaa  2957  r19.30  3079  trint  4733  mpteqb  6256  tz7.49  7486  mptelixpg  7890  resixpfo  7891  bnd  8700  kmlem12  8928  lbzbi  11720  r19.29uz  14019  caubnd  14027  alzdvds  14961  ptclsg  21323  isucn2  21988  fusgreghash2wsp  27054  omssubadd  30135  dfon2lem8  31384  dford3lem2  37041  neik0pk1imk0  37794
  Copyright terms: Public domain W3C validator