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

Theorem ralimdaa 3248
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 411 . . 3 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
41, 3ralrimi 3245 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
5 ralim 3076 . 2 (∀𝑥𝐴 (𝜓𝜒) → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
64, 5syl 17 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  wnf 1778  wcel 2099  wral 3051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-12 2167
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-nf 1779  df-ral 3052
This theorem is referenced by:  ralbida  3258  eltsk2g  10785  ptcnplem  23613  poimirlem26  37360  allbutfifvre  45332  climleltrp  45333  fnlimabslt  45336  limsupub2  45469  liminflbuz2  45472  xlimmnfvlem1  45489  xlimmnfvlem2  45490  xlimpnfvlem1  45493  xlimpnfvlem2  45494  stoweidlem61  45718  stoweid  45720  fourierdlem73  45836  smflimlem2  46429
  Copyright terms: Public domain W3C validator