Metamath Proof Explorer


Theorem pm13.194

Description: Theorem *13.194 in WhiteheadRussell p. 179. (Contributed by Andrew Salmon, 3-Jun-2011)

Ref Expression
Assertion pm13.194 φx=yyxφφx=y

Proof

Step Hyp Ref Expression
1 pm13.13a φx=y[˙y/x]˙φ
2 sbsbc yxφ[˙y/x]˙φ
3 1 2 sylibr φx=yyxφ
4 simpl φx=yφ
5 simpr φx=yx=y
6 3 4 5 3jca φx=yyxφφx=y
7 3simpc yxφφx=yφx=y
8 6 7 impbii φx=yyxφφx=y