Metamath Proof Explorer


Theorem wl-sbcom2d-lem1

Description: Lemma used to prove wl-sbcom2d . (Contributed by Wolf Lammen, 10-Aug-2019) (New usage is discouraged.)

Ref Expression
Assertion wl-sbcom2d-lem1 u=yv=w¬xx=wuxvzφyxwzφ

Proof

Step Hyp Ref Expression
1 nfna1 x¬xx=w
2 nfeqf2 ¬xx=wxv=w
3 1 2 nfan1 x¬xx=wv=w
4 sbequ v=wvzφwzφ
5 4 adantl ¬xx=wv=wvzφwzφ
6 3 5 sbbid ¬xx=wv=wuxvzφuxwzφ
7 6 ancoms v=w¬xx=wuxvzφuxwzφ
8 sbequ u=yuxwzφyxwzφ
9 7 8 sylan9bbr u=yv=w¬xx=wuxvzφyxwzφ
10 9 expr u=yv=w¬xx=wuxvzφyxwzφ