Metamath Proof Explorer


Theorem sbco2vv

Description: A composition law for substitution. Version of sbco2 with disjoint variable conditions and fewer axioms. (Contributed by NM, 30-Jun-1994) (Revised by BJ, 22-Dec-2020) (Proof shortened by Wolf Lammen, 29-Apr-2023)

Ref Expression
Assertion sbco2vv y z z x φ y x φ

Proof

Step Hyp Ref Expression
1 sbequ z = w z x φ w x φ
2 sbequ w = y w x φ y x φ
3 1 2 sbievw2 y z z x φ y x φ