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

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

Proof of Theorem rsp2
StepHypRef Expression
1 rsp 3172 . . 3 (∀𝑥𝐴𝑦𝐵 𝜑 → (𝑥𝐴 → ∀𝑦𝐵 𝜑))
2 rsp 3172 . . 3 (∀𝑦𝐵 𝜑 → (𝑦𝐵𝜑))
31, 2syl6 35 . 2 (∀𝑥𝐴𝑦𝐵 𝜑 → (𝑥𝐴 → (𝑦𝐵𝜑)))
43impd 411 1 (∀𝑥𝐴𝑦𝐵 𝜑 → ((𝑥𝐴𝑦𝐵) → 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2081  wral 3105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-12 2141
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-ral 3110
This theorem is referenced by:  ralcom2  3324  disjxiun  4959  solin  5386  mpocurryd  7786  cmncom  18649  cnmpt21  21963  cnmpt2t  21965  cnmpt22  21966  cnmptcom  21970  frgrwopreglem5ALT  27793  htthlem  28385  cplgredgex  31979  prtlem14  35560  islptre  41461  sprsymrelfolem2  43157
  Copyright terms: Public domain W3C validator