Metamath Proof Explorer


Theorem sbcco3g

Description: Composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker sbcco3gw when possible. (Contributed by NM, 27-Nov-2005) (Revised by Mario Carneiro, 11-Nov-2016) (New usage is discouraged.)

Ref Expression
Hypothesis sbcco3g.1 x=AB=C
Assertion sbcco3g AV[˙A/x]˙[˙B/y]˙φ[˙C/y]˙φ

Proof

Step Hyp Ref Expression
1 sbcco3g.1 x=AB=C
2 sbcnestg AV[˙A/x]˙[˙B/y]˙φ[˙A/xB/y]˙φ
3 elex AVAV
4 nfcvd AV_xC
5 4 1 csbiegf AVA/xB=C
6 dfsbcq A/xB=C[˙A/xB/y]˙φ[˙C/y]˙φ
7 3 5 6 3syl AV[˙A/xB/y]˙φ[˙C/y]˙φ
8 2 7 bitrd AV[˙A/x]˙[˙B/y]˙φ[˙C/y]˙φ