Metamath Proof Explorer


Theorem breqd

Description: Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011)

Ref Expression
Hypothesis breq1d.1 φ A = B
Assertion breqd φ C A D C B D

Proof

Step Hyp Ref Expression
1 breq1d.1 φ A = B
2 breq A = B C A D C B D
3 1 2 syl φ C A D C B D