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

Theorem ralim 3166
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 3160 1 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wral 3142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 208  df-ral 3147
This theorem is referenced by:  ralimdaa  3221  r19.30  3342  r19.30OLD  3343  mpteqb  6782  tz7.49  8075  mptelixpg  8491  resixpfo  8492  bnd  9313  kmlem12  9579  lbzbi  12328  r19.29uz  14703  caubnd  14711  alzdvds  15663  ptclsg  22142  isucn2  22806  fusgreghash2wsp  28034  omssubadd  31447  subgrwlk  32266  dfon2lem8  32922  fvineqsneq  34565  dford3lem2  39492  neik0pk1imk0  40265  grur1cld  40436  mnuprdlem4  40479  mnurndlem1  40485
  Copyright terms: Public domain W3C validator