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 ] ph <-> [ z / y ] [ z / x ] ph )

Proof

Step	Hyp	Ref	Expression
1		nfa1	|- F/ y A. y y = z
2		drsb2	|- ( A. y y = z -> ( [ y / x ] ph <-> [ z / x ] ph ) )
3	1 2	sbbid	|- ( A. y y = z -> ( [ z / y ] [ y / x ] ph <-> [ z / y ] [ z / x ] ph ) )
4		sb4b	|- ( -. A. y y = z -> ( [ z / y ] [ y / x ] ph <-> A. y ( y = z -> [ y / x ] ph ) ) )
5		sbequ	|- ( y = z -> ( [ y / x ] ph <-> [ z / x ] ph ) )
6	5	pm5.74i	|- ( ( y = z -> [ y / x ] ph ) <-> ( y = z -> [ z / x ] ph ) )
7	6	albii	|- ( A. y ( y = z -> [ y / x ] ph ) <-> A. y ( y = z -> [ z / x ] ph ) )
8	4 7	bitrdi	|- ( -. A. y y = z -> ( [ z / y ] [ y / x ] ph <-> A. y ( y = z -> [ z / x ] ph ) ) )
9		sb4b	|- ( -. A. y y = z -> ( [ z / y ] [ z / x ] ph <-> A. y ( y = z -> [ z / x ] ph ) ) )
10	8 9	bitr4d	|- ( -. A. y y = z -> ( [ z / y ] [ y / x ] ph <-> [ z / y ] [ z / x ] ph ) )
11	3 10	pm2.61i	|- ( [ z / y ] [ y / x ] ph <-> [ z / y ] [ z / x ] ph )