Metamath Proof Explorer


Theorem cdeqi

Description: Deduce conditional equality. (Contributed by Mario Carneiro, 11-Aug-2016)

Ref Expression
Hypothesis cdeqi.1 x=yφ
Assertion cdeqi CondEqx=yφ

Proof

Step Hyp Ref Expression
1 cdeqi.1 x=yφ
2 df-cdeq CondEqx=yφx=yφ
3 1 2 mpbir CondEqx=yφ