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

Theorem rsp2 2920
 Description: Restricted specialization, with two quantifiers. (Contributed by NM, 11-Feb-1997.)
Assertion
Ref Expression
rsp2 (∀𝑥𝐴𝑦𝐵 𝜑 → ((𝑥𝐴𝑦𝐵) → 𝜑))

Proof of Theorem rsp2
StepHypRef Expression
1 rsp 2913 . . 3 (∀𝑥𝐴𝑦𝐵 𝜑 → (𝑥𝐴 → ∀𝑦𝐵 𝜑))
2 rsp 2913 . . 3 (∀𝑦𝐵 𝜑 → (𝑦𝐵𝜑))
31, 2syl6 34 . 2 (∀𝑥𝐴𝑦𝐵 𝜑 → (𝑥𝐴 → (𝑦𝐵𝜑)))
43impd 446 1 (∀𝑥𝐴𝑦𝐵 𝜑 → ((𝑥𝐴𝑦𝐵) → 𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ∀wral 2896 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901 This theorem is referenced by:  ralcom2  3083  disjxiun  4579  disjxiunOLD  4580  solin  4982  mpt2curryd  7282  cmncom  18032  cnmpt21  21284  cnmpt2t  21286  cnmpt22  21287  cnmptcom  21291  frgrawopreglem5  26575  htthlem  27158  prtlem14  33177  islptre  38686  frgrwopreglem5  41485
 Copyright terms: Public domain W3C validator