Metamath Proof Explorer

Theorem sbcom3vv

Description: Substituting y for x and then z for y is equivalent to substituting z for both x and y . Version of sbcom3 with a disjoint variable condition using fewer axioms. (Contributed by NM, 27-May-1997) (Revised by Giovanni Mascellani, 8-Apr-2018) (Revised by BJ, 30-Dec-2020) (Proof shortened by Wolf Lammen, 19-Jan-2023)

Ref Expression
Assertion sbcom3vv ⊢ z y y x φ ↔ z y z x φ

Proof

Step Hyp Ref Expression
1 sbequ ⊢ y = z → y x φ ↔ z x φ
2 1 pm5.74i ⊢ y = z → y x φ ↔ y = z → z x φ
3 2 albii ⊢ ∀ y y = z → y x φ ↔ ∀ y y = z → z x φ
4 sb6 ⊢ z y y x φ ↔ ∀ y y = z → y x φ
5 sb6 ⊢ z y z x φ ↔ ∀ y y = z → z x φ
6 3 4 5 3bitr4i ⊢ z y y x φ ↔ z y z x φ