Metamath Proof Explorer

Theorem sbcom4

Description: Commutativity law for substitution. This theorem was incorrectly used as our previous version of pm11.07 but may still be useful. (Contributed by Andrew Salmon, 17-Jun-2011) (Proof shortened by Jim Kingdon, 22-Jan-2018)

Ref Expression
Assertion sbcom4 w x y z φ y x w z φ


Step Hyp Ref Expression
1 sbv w x φ φ
2 sbv y z φ φ
3 2 sbbii w x y z φ w x φ
4 sbv w z φ φ
5 4 sbbii y x w z φ y x φ
6 sbv y x φ φ
7 5 6 bitri y x w z φ φ
8 1 3 7 3bitr4i w x y z φ y x w z φ