Metamath Proof Explorer


Theorem breqan12d

Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996)

Ref Expression
Hypotheses breq1d.1 φA=B
breqan12i.2 ψC=D
Assertion breqan12d φψARCBRD

Proof

Step Hyp Ref Expression
1 breq1d.1 φA=B
2 breqan12i.2 ψC=D
3 breq12 A=BC=DARCBRD
4 1 2 3 syl2an φψARCBRD