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

Theorem ralim 3094
 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 3088 1 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wral 3070 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 210  df-ral 3075 This theorem is referenced by:  ralimdaa  3145  r19.30  3258  mpteqb  6778  tz7.49  8091  mptelixpg  8517  resixpfo  8518  bnd  9354  kmlem12  9621  lbzbi  12376  r19.29uz  14758  caubnd  14766  alzdvds  15721  ptclsg  22315  isucn2  22980  fusgreghash2wsp  28222  omssubadd  31786  subgrwlk  32610  dfon2lem8  33282  fvineqsneq  35109  dford3lem2  40341  neik0pk1imk0  41123  grur1cld  41313  mnuprdlem4  41356  mnurndlem1  41362
 Copyright terms: Public domain W3C validator