Metamath Proof Explorer


Theorem breqdi

Description: Equality deduction for a binary relation. (Contributed by Thierry Arnoux, 5-Oct-2020)

Ref Expression
Hypotheses breq1d.1
|- ( ph -> A = B )
breqdi.1
|- ( ph -> C A D )
Assertion breqdi
|- ( ph -> C B D )

Proof

Step Hyp Ref Expression
1 breq1d.1
 |-  ( ph -> A = B )
2 breqdi.1
 |-  ( ph -> C A D )
3 1 breqd
 |-  ( ph -> ( C A D <-> C B D ) )
4 2 3 mpbid
 |-  ( ph -> C B D )