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

Theorem ralim 3159
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 3153 1 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wral 3135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801
This theorem depends on definitions:  df-bi 208  df-ral 3140
This theorem is referenced by:  ralimdaa  3214  r19.30  3335  r19.30OLD  3336  mpteqb  6779  tz7.49  8070  mptelixpg  8487  resixpfo  8488  bnd  9309  kmlem12  9575  lbzbi  12324  r19.29uz  14698  caubnd  14706  alzdvds  15658  ptclsg  22151  isucn2  22815  fusgreghash2wsp  28044  omssubadd  31457  subgrwlk  32276  dfon2lem8  32932  fvineqsneq  34575  dford3lem2  39502  neik0pk1imk0  40275  grur1cld  40445  mnuprdlem4  40488  mnurndlem1  40494
  Copyright terms: Public domain W3C validator