Metamath Proof Explorer


Theorem frege55lem1b

Description: Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019)

Ref Expression
Assertion frege55lem1b φ x y y = z φ x = z

Proof

Step Hyp Ref Expression
1 equsb3 x y y = z x = z
2 1 biimpi x y y = z x = z
3 2 imim2i φ x y y = z φ x = z