Metamath Proof Explorer


Theorem 2sb6rf

Description: Reversed double substitution. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 3-Feb-2005) (Revised by Mario Carneiro, 6-Oct-2016) Remove variable constraints. (Revised by Wolf Lammen, 28-Sep-2018) (Proof shortened by Wolf Lammen, 13-Apr-2023) (New usage is discouraged.)

Ref Expression
Hypotheses 2sb5rf.1 z φ
2sb5rf.2 w φ
Assertion 2sb6rf φ z w z = x w = y z x w y φ

Proof

Step Hyp Ref Expression
1 2sb5rf.1 z φ
2 2sb5rf.2 w φ
3 1 19.23 z w z = x w = y φ z w z = x w = y φ
4 2 19.23 w z = x w = y φ w z = x w = y φ
5 4 albii z w z = x w = y φ z w z = x w = y φ
6 2ax6e z w z = x w = y
7 6 a1bi φ z w z = x w = y φ
8 3 5 7 3bitr4ri φ z w z = x w = y φ
9 sbequ12r z = x z x w y φ w y φ
10 sbequ12r w = y w y φ φ
11 9 10 sylan9bb z = x w = y z x w y φ φ
12 11 pm5.74i z = x w = y z x w y φ z = x w = y φ
13 12 2albii z w z = x w = y z x w y φ z w z = x w = y φ
14 8 13 bitr4i φ z w z = x w = y z x w y φ