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

Theorem ralim 3084
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 3083 1 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wral 3059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806
This theorem depends on definitions:  df-bi 207  df-ral 3060
This theorem is referenced by:  r19.30OLD  3119  ralimdaa  3258  mpteqb  7035  tz7.49  8484  mptelixpg  8974  resixpfo  8975  bnd  9930  kmlem12  10200  lbzbi  12976  r19.29uz  15386  caubnd  15394  alzdvds  16354  ptclsg  23639  isucn2  24304  fusgreghash2wsp  30367  omssubadd  34282  subgrwlk  35117  dfon2lem8  35772  fvineqsneq  37395  dford3lem2  43016  neik0pk1imk0  44037  grur1cld  44228  mnuprdlem4  44271  mnurndlem1  44277
  Copyright terms: Public domain W3C validator