Metamath Proof Explorer

Theorem frege55lem1b

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

Ref Expression
Assertion frege55lem1b ( ( 𝜑 → [ 𝑥 / 𝑦 ] 𝑦 = 𝑧 ) → ( 𝜑 → 𝑥 = 𝑧 ) )

Proof

Step Hyp Ref Expression
1 equsb3 ⊢ ( [ 𝑥 / 𝑦 ] 𝑦 = 𝑧 ↔ 𝑥 = 𝑧 )
2 1 biimpi ⊢ ( [ 𝑥 / 𝑦 ] 𝑦 = 𝑧 → 𝑥 = 𝑧 )
3 2 imim2i ⊢ ( ( 𝜑 → [ 𝑥 / 𝑦 ] 𝑦 = 𝑧 ) → ( 𝜑 → 𝑥 = 𝑧 ) )