Theorem breq123d 4466

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

Hypotheses

Ref	Expression
breq1d.1
breq123d.2
breq123d.3

Assertion

Ref	Expression
breq123d

Proof of Theorem breq123d

Step	Hyp	Ref	Expression
1		breq1d.1	. . 3
2		breq123d.3	. . 3
3	1, 2	breq12d 4465	. 2
4		breq123d.2	. . 3
5	4	breqd 4463	. 2
6	3, 5	bitrd 253	1

Syntax hints:  ->wi 4  <->wb 184  =wceq 1395   class class class wbr 4452

This theorem is referenced by:  sbcbr123  4503  sbcbrgOLD  4504  fmptco  6064  xpsle  14978  invfuc  15343  yonedainv  15550  opphllem3  24121  lmif  24151  islmib  24153  fmptcof2  27502  submomnd  27700  sgnsv  27717  inftmrel  27724  isinftm  27725  submarchi  27730  suborng  27805  fnwe2val  30995  aomclem8  31007  iscvlat  35048  paddfval  35521  lhpset  35719  tendofset  36484  diaffval  36757

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453