Metamath Proof Explorer

Theorem breq12i

Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996) (Proof shortened by Eric Schmidt, 4-Apr-2007)

Ref Expression
Hypotheses breq1i.1 
|- A = B
breq12i.2 
|- C = D
Assertion breq12i 
|- ( A R C <-> B R D )

Proof

Step Hyp Ref Expression
1 breq1i.1 
 |-  A = B
2 breq12i.2 
 |-  C = D
3 breq12 
 |-  ( ( A = B /\ C = D ) -> ( A R C <-> B R D ) )
4 1 2 3 mp2an 
 |-  ( A R C <-> B R D )