Theorem sbco2

Description: A composition law for substitution. For versions requiring fewer axioms, but more disjoint variable conditions, see sbco2v and sbco2vv . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 30-Jun-1994) (Revised by Mario Carneiro, 6-Oct-2016) (Proof shortened by Wolf Lammen, 17-Sep-2018) (New usage is discouraged.)

	Ref	Expression
Hypothesis	sbco2.1	$$⊢Ⅎz\phi$$
Assertion	sbco2	$$⊢\left[y/z\right]\left[z/x\right]\phi \leftrightarrow \left[y/x\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		sbco2.1	$$⊢Ⅎz\phi$$
2		sbequ12	$$⊢z=y\to \left(\left[z/x\right]\phi \leftrightarrow \left[y/z\right]\left[z/x\right]\phi \right)$$
3		sbequ	$$⊢z=y\to \left(\left[z/x\right]\phi \leftrightarrow \left[y/x\right]\phi \right)$$
4	2 3	bitr3d	$$⊢z=y\to \left(\left[y/z\right]\left[z/x\right]\phi \leftrightarrow \left[y/x\right]\phi \right)$$
5	4	sps	$$⊢\forall zz=y\to \left(\left[y/z\right]\left[z/x\right]\phi \leftrightarrow \left[y/x\right]\phi \right)$$
6		nfnae	$$⊢Ⅎz\neg \forall zz=y$$
7	1	nfsb4	$$⊢\neg \forall zz=y\to Ⅎz\left[y/x\right]\phi$$
8	3	a1i	$$⊢\neg \forall zz=y\to \left(z=y\to \left(\left[z/x\right]\phi \leftrightarrow \left[y/x\right]\phi \right)\right)$$
9	6 7 8	sbied	$$⊢\neg \forall zz=y\to \left(\left[y/z\right]\left[z/x\right]\phi \leftrightarrow \left[y/x\right]\phi \right)$$
10	5 9	pm2.61i	$$⊢\left[y/z\right]\left[z/x\right]\phi \leftrightarrow \left[y/x\right]\phi$$