Theorem sbco3

Description: A composition law for substitution. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 2-Jun-1993) (Proof shortened by Wolf Lammen, 18-Sep-2018) (New usage is discouraged.)

	Ref	Expression
Assertion	sbco3	|- ( [ z / y ] [ y / x ] ph <-> [ z / x ] [ x / y ] ph )

Proof

Step	Hyp	Ref	Expression
1		drsb1	|- ( A. x x = y -> ( [ z / x ] [ y / x ] ph <-> [ z / y ] [ y / x ] ph ) )
2		nfae	|- F/ x A. x x = y
3		sbequ12a	|- ( x = y -> ( [ y / x ] ph <-> [ x / y ] ph ) )
4	3	sps	|- ( A. x x = y -> ( [ y / x ] ph <-> [ x / y ] ph ) )
5	2 4	sbbid	|- ( A. x x = y -> ( [ z / x ] [ y / x ] ph <-> [ z / x ] [ x / y ] ph ) )
6	1 5	bitr3d	|- ( A. x x = y -> ( [ z / y ] [ y / x ] ph <-> [ z / x ] [ x / y ] ph ) )
7		nfnae	|- F/ y -. A. x x = y
8		nfnae	|- F/ x -. A. x x = y
9		nfsb2	|- ( -. A. x x = y -> F/ x [ y / x ] ph )
10	7 8 9	sbco2d	|- ( -. A. x x = y -> ( [ z / x ] [ x / y ] [ y / x ] ph <-> [ z / y ] [ y / x ] ph ) )
11		sbco	|- ( [ x / y ] [ y / x ] ph <-> [ x / y ] ph )
12	11	sbbii	|- ( [ z / x ] [ x / y ] [ y / x ] ph <-> [ z / x ] [ x / y ] ph )
13	10 12	bitr3di	|- ( -. A. x x = y -> ( [ z / y ] [ y / x ] ph <-> [ z / x ] [ x / y ] ph ) )
14	6 13	pm2.61i	|- ( [ z / y ] [ y / x ] ph <-> [ z / x ] [ x / y ] ph )