Metamath Proof Explorer

Theorem sbcom3

Description: Substituting y for x and then z for y is equivalent to substituting z for both x and y . Usage of this theorem is discouraged because it depends on ax-13 . For a version requiring a disjoint variable, but fewer axioms, see sbcom3vv . (Contributed by Giovanni Mascellani, 8-Apr-2018) Remove dependency on ax-11 . (Revised by Wolf Lammen, 16-Sep-2018) (Proof shortened by Wolf Lammen, 16-Sep-2018) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 nfa1 ⊢ Ⅎ y ∀ y y = z
2 drsb2 ⊢ ∀ y y = z → y x φ ↔ z x φ
3 1 2 sbbid ⊢ ∀ y y = z → z y y x φ ↔ z y z x φ
4 sb4b ⊢ ¬ ∀ y y = z → z y y x φ ↔ ∀ y y = z → y x φ
5 sbequ ⊢ y = z → y x φ ↔ z x φ
6 5 pm5.74i ⊢ y = z → y x φ ↔ y = z → z x φ
7 6 albii ⊢ ∀ y y = z → y x φ ↔ ∀ y y = z → z x φ
8 4 7 bitrdi ⊢ ¬ ∀ y y = z → z y y x φ ↔ ∀ y y = z → z x φ
9 sb4b ⊢ ¬ ∀ y y = z → z y z x φ ↔ ∀ y y = z → z x φ
10 8 9 bitr4d ⊢ ¬ ∀ y y = z → z y y x φ ↔ z y z x φ
11 3 10 pm2.61i ⊢ z y y x φ ↔ z y z x φ