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 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-ral 3062
This theorem is referenced by:  r19.30OLD  3121  ralimdaa  3260  mpteqb  7035  tz7.49  8485  mptelixpg  8975  resixpfo  8976  bnd  9932  kmlem12  10202  lbzbi  12978  r19.29uz  15389  caubnd  15397  alzdvds  16357  ptclsg  23623  isucn2  24288  fusgreghash2wsp  30357  omssubadd  34302  subgrwlk  35137  dfon2lem8  35791  fvineqsneq  37413  dford3lem2  43039  neik0pk1imk0  44060  grur1cld  44251  mnuprdlem4  44294  mnurndlem1  44300
  Copyright terms: Public domain W3C validator