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

Theorem ralimdaa 3256
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 412 . . 3 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
41, 3ralrimi 3253 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
5 ralim 3085 . 2 (∀𝑥𝐴 (𝜓𝜒) → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
64, 5syl 17 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wnf 1784  wcel 2105  wral 3060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-12 2170
This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-nf 1785  df-ral 3061
This theorem is referenced by:  ralbida  3266  eltsk2g  10749  ptcnplem  23346  poimirlem26  36818  allbutfifvre  44691  climleltrp  44692  fnlimabslt  44695  limsupub2  44828  liminflbuz2  44831  xlimmnfvlem1  44848  xlimmnfvlem2  44849  xlimpnfvlem1  44852  xlimpnfvlem2  44853  stoweidlem61  45077  stoweid  45079  fourierdlem73  45195  smflimlem2  45788
  Copyright terms: Public domain W3C validator