Metamath Proof Explorer


Theorem sbft

Description: Substitution has no effect on a nonfree variable. (Contributed by NM, 30-May-2009) (Revised by Mario Carneiro, 12-Oct-2016) (Proof shortened by Wolf Lammen, 3-May-2018)

Ref Expression
Assertion sbft x φ y x φ φ

Proof

Step Hyp Ref Expression
1 spsbe y x φ x φ
2 19.9t x φ x φ φ
3 1 2 syl5ib x φ y x φ φ
4 nf5r x φ φ x φ
5 stdpc4 x φ y x φ
6 4 5 syl6 x φ φ y x φ
7 3 6 impbid x φ y x φ φ