Metamath Proof Explorer


Theorem breq123d

Description: Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011)

Ref Expression
Hypotheses breq1d.1 φA=B
breq123d.2 φR=S
breq123d.3 φC=D
Assertion breq123d φARCBSD

Proof

Step Hyp Ref Expression
1 breq1d.1 φA=B
2 breq123d.2 φR=S
3 breq123d.3 φC=D
4 1 3 breq12d φARCBRD
5 2 breqd φBRDBSD
6 4 5 bitrd φARCBSD