Metamath Proof Explorer

Theorem 3brtr3g

Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997)

Ref Expression
Hypotheses 3brtr3g.1 φ A R B
3brtr3g.2 A = C
3brtr3g.3 B = D
Assertion 3brtr3g φ C R D


Step Hyp Ref Expression
1 3brtr3g.1 φ A R B
2 3brtr3g.2 A = C
3 3brtr3g.3 B = D
4 2 3 breq12i A R B C R D
5 1 4 sylib φ C R D