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 CondEq x = y φ

Proof

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