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

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

Proof of Theorem rsp2
StepHypRef Expression
1 rsp 3134 . . 3 (∀𝑥𝐴𝑦𝐵 𝜑 → (𝑥𝐴 → ∀𝑦𝐵 𝜑))
2 rsp 3134 . . 3 (∀𝑦𝐵 𝜑 → (𝑦𝐵𝜑))
31, 2syl6 35 . 2 (∀𝑥𝐴𝑦𝐵 𝜑 → (𝑥𝐴 → (𝑦𝐵𝜑)))
43impd 414 1 (∀𝑥𝐴𝑦𝐵 𝜑 → ((𝑥𝐴𝑦𝐵) → 𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  ∀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  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2175 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3075 This theorem is referenced by:  ralcom2  3281  disjxiun  5029  solin  5467  mpocurryd  7945  cmncom  18990  cnmpt21  22371  cnmpt2t  22373  cnmpt22  22374  cnmptcom  22378  frgrwopreglem5ALT  28206  htthlem  28799  qsidomlem2  31150  cplgredgex  32598  prtlem14  36450  islptre  42627  sprsymrelfolem2  44378
 Copyright terms: Public domain W3C validator