Metamath Proof Explorer

Theorem breq12d

Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996) (Proof shortened by Andrew Salmon, 9-Jul-2011)

Ref Expression
Hypotheses breq1d.1 
|- ( ph -> A = B )
breq12d.2 
|- ( ph -> C = D )
Assertion breq12d 
|- ( ph -> ( A R C <-> B R D ) )

Proof

Step Hyp Ref Expression
1 breq1d.1 
 |-  ( ph -> A = B )
2 breq12d.2 
 |-  ( ph -> C = D )
3 breq12 
 |-  ( ( A = B /\ C = D ) -> ( A R C <-> B R D ) )
4 1 2 3 syl2anc 
 |-  ( ph -> ( A R C <-> B R D ) )