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

Theorem ralim 3086
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 3085 1 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811
This theorem depends on definitions:  df-bi 206  df-ral 3062
This theorem is referenced by:  r19.30OLD  3121  ralimdaa  3257  mpteqb  7014  tz7.49  8441  mptelixpg  8925  resixpfo  8926  bnd  9883  kmlem12  10152  lbzbi  12916  r19.29uz  15293  caubnd  15301  alzdvds  16259  ptclsg  23110  isucn2  23775  fusgreghash2wsp  29580  omssubadd  33287  subgrwlk  34111  dfon2lem8  34750  fvineqsneq  36281  dford3lem2  41751  neik0pk1imk0  42783  grur1cld  42976  mnuprdlem4  43019  mnurndlem1  43025
  Copyright terms: Public domain W3C validator