Metamath Proof Explorer


Theorem drsb1

Description: Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of Megill p. 448 (p. 16 of preprint). Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 2-Jun-1993) (New usage is discouraged.)

Ref Expression
Assertion drsb1 xx=yzxφzyφ

Proof

Step Hyp Ref Expression
1 equequ1 x=yx=zy=z
2 1 sps xx=yx=zy=z
3 2 imbi1d xx=yx=zφy=zφ
4 2 anbi1d xx=yx=zφy=zφ
5 4 drex1 xx=yxx=zφyy=zφ
6 3 5 anbi12d xx=yx=zφxx=zφy=zφyy=zφ
7 dfsb1 zxφx=zφxx=zφ
8 dfsb1 zyφy=zφyy=zφ
9 6 7 8 3bitr4g xx=yzxφzyφ