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

Theorem ralimdaa 3258
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-Sep-2003.) (Proof shortened by Wolf Lammen, 29-Dec-2019.)
Hypotheses
Ref Expression
ralimdaa.1 𝑥𝜑
ralimdaa.2 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
ralimdaa (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))

Proof of Theorem ralimdaa
StepHypRef Expression
1 ralimdaa.1 . . 3 𝑥𝜑
2 ralimdaa.2 . . . 4 ((𝜑𝑥𝐴) → (𝜓𝜒))
32ex 414 . . 3 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
41, 3ralrimi 3255 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
5 ralim 3087 . 2 (∀𝑥𝐴 (𝜓𝜒) → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
64, 5syl 17 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wnf 1786  wcel 2107  wral 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-nf 1787  df-ral 3063
This theorem is referenced by:  ralbida  3268  eltsk2g  10746  ptcnplem  23125  poimirlem26  36514  allbutfifvre  44391  climleltrp  44392  fnlimabslt  44395  limsupub2  44528  liminflbuz2  44531  xlimmnfvlem1  44548  xlimmnfvlem2  44549  xlimpnfvlem1  44552  xlimpnfvlem2  44553  stoweidlem61  44777  stoweid  44779  fourierdlem73  44895  smflimlem2  45488
  Copyright terms: Public domain W3C validator