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	$$⊢Ⅎx\phi$$
	sbco2d.2	$$⊢Ⅎz\phi$$
	sbco2d.3	$$⊢\phi \to Ⅎz\psi$$
Assertion	sbco2d	$$⊢\phi \to \left(\left[y/z\right]\left[z/x\right]\psi \leftrightarrow \left[y/x\right]\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sbco2d.1	$$⊢Ⅎx\phi$$
2		sbco2d.2	$$⊢Ⅎz\phi$$
3		sbco2d.3	$$⊢\phi \to Ⅎz\psi$$
4	2 3	nfim1	$$⊢Ⅎz\left(\phi \to \psi \right)$$
5	4	sbco2	$$⊢\left[y/z\right]\left[z/x\right]\left(\phi \to \psi \right)\leftrightarrow \left[y/x\right]\left(\phi \to \psi \right)$$
6	1	sbrim	$$⊢\left[z/x\right]\left(\phi \to \psi \right)\leftrightarrow \left(\phi \to \left[z/x\right]\psi \right)$$
7	6	sbbii	$$⊢\left[y/z\right]\left[z/x\right]\left(\phi \to \psi \right)\leftrightarrow \left[y/z\right]\left(\phi \to \left[z/x\right]\psi \right)$$
8	2	sbrim	$$⊢\left[y/z\right]\left(\phi \to \left[z/x\right]\psi \right)\leftrightarrow \left(\phi \to \left[y/z\right]\left[z/x\right]\psi \right)$$
9	7 8	bitri	$$⊢\left[y/z\right]\left[z/x\right]\left(\phi \to \psi \right)\leftrightarrow \left(\phi \to \left[y/z\right]\left[z/x\right]\psi \right)$$
10	1	sbrim	$$⊢\left[y/x\right]\left(\phi \to \psi \right)\leftrightarrow \left(\phi \to \left[y/x\right]\psi \right)$$
11	5 9 10	3bitr3i	$$⊢\left(\phi \to \left[y/z\right]\left[z/x\right]\psi \right)\leftrightarrow \left(\phi \to \left[y/x\right]\psi \right)$$
12	11	pm5.74ri	$$⊢\phi \to \left(\left[y/z\right]\left[z/x\right]\psi \leftrightarrow \left[y/x\right]\psi \right)$$