Metamath Proof Explorer


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φ
Assertion sbco2 yzzxφyxφ

Proof

Step Hyp Ref Expression
1 sbco2.1 zφ
2 sbequ12 z=yzxφyzzxφ
3 sbequ z=yzxφyxφ
4 2 3 bitr3d z=yyzzxφyxφ
5 4 sps zz=yyzzxφyxφ
6 nfnae z¬zz=y
7 1 nfsb4 ¬zz=yzyxφ
8 3 a1i ¬zz=yz=yzxφyxφ
9 6 7 8 sbied ¬zz=yyzzxφyxφ
10 5 9 pm2.61i yzzxφyxφ