Theorem sbco2d

Description: A composition law for substitution. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 2-Jun-1993) (Revised by Mario Carneiro, 6-Oct-2016) (New usage is discouraged.)

	Ref	Expression
Hypotheses	sbco2d.1	|- F/ x ph
	sbco2d.2	|- F/ z ph
	sbco2d.3	|- ( ph -> F/ z ps )
Assertion	sbco2d	|- ( ph -> ( [ y / z ] [ z / x ] ps <-> [ y / x ] ps ) )

Proof

Step	Hyp	Ref	Expression
1		sbco2d.1	|- F/ x ph
2		sbco2d.2	|- F/ z ph
3		sbco2d.3	|- ( ph -> F/ z ps )
4	2 3	nfim1	|- F/ z ( ph -> ps )
5	4	sbco2	|- ( [ y / z ] [ z / x ] ( ph -> ps ) <-> [ y / x ] ( ph -> ps ) )
6	1	sbrim	|- ( [ z / x ] ( ph -> ps ) <-> ( ph -> [ z / x ] ps ) )
7	6	sbbii	|- ( [ y / z ] [ z / x ] ( ph -> ps ) <-> [ y / z ] ( ph -> [ z / x ] ps ) )
8	2	sbrim	|- ( [ y / z ] ( ph -> [ z / x ] ps ) <-> ( ph -> [ y / z ] [ z / x ] ps ) )
9	7 8	bitri	|- ( [ y / z ] [ z / x ] ( ph -> ps ) <-> ( ph -> [ y / z ] [ z / x ] ps ) )
10	1	sbrim	|- ( [ y / x ] ( ph -> ps ) <-> ( ph -> [ y / x ] ps ) )
11	5 9 10	3bitr3i	|- ( ( ph -> [ y / z ] [ z / x ] ps ) <-> ( ph -> [ y / x ] ps ) )
12	11	pm5.74ri	|- ( ph -> ( [ y / z ] [ z / x ] ps <-> [ y / x ] ps ) )