Metamath Proof Explorer

Theorem breq2d

Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996)

Ref Expression
Hypothesis breq1d.1 
|- ( ph -> A = B )
Assertion breq2d 
|- ( ph -> ( C R A <-> C R B ) )

Proof

Step Hyp Ref Expression
1 breq1d.1 
 |-  ( ph -> A = B )
2 breq2 
 |-  ( A = B -> ( C R A <-> C R B ) )
3 1 2 syl 
 |-  ( ph -> ( C R A <-> C R B ) )