New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  rsp2e GIF version

Theorem rsp2e 2677
 Description: Restricted specialization. (Contributed by FL, 4-Jun-2012.)
Assertion
Ref Expression
rsp2e ((x A y B φ) → x A y B φ)

Proof of Theorem rsp2e
StepHypRef Expression
1 simp1 955 . . 3 ((x A y B φ) → x A)
2 rspe 2675 . . . 4 ((y B φ) → y B φ)
323adant1 973 . . 3 ((x A y B φ) → y B φ)
4 19.8a 1756 . . 3 ((x A y B φ) → x(x A y B φ))
51, 3, 4syl2anc 642 . 2 ((x A y B φ) → x(x A y B φ))
6 df-rex 2620 . 2 (x A y B φx(x A y B φ))
75, 6sylibr 203 1 ((x A y B φ) → x A y B φ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 358   ∧ w3a 934  ∃wex 1541   ∈ wcel 1710  ∃wrex 2615 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746 This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-ex 1542  df-rex 2620 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator