Metamath Proof Explorer

Theorem 3brtr3d

Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 18-Oct-1999)

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


Step Hyp Ref Expression
1 3brtr3d.1 φ A R B
2 3brtr3d.2 φ A = C
3 3brtr3d.3 φ B = D
4 2 3 breq12d φ A R B C R D
5 1 4 mpbid φ C R D