Theorem breqtri 4475

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)

Hypotheses

Ref	Expression
breqtr.1
breqtr.2

Assertion

Ref	Expression
breqtri

Proof of Theorem breqtri

Step	Hyp	Ref	Expression
1		breqtr.1	. 2
2		breqtr.2	. . 3
3	2	breq2i 4460	. 2
4	1, 3	mpbi 208	1

Syntax hints:  =wceq 1395   class class class wbr 4452

This theorem is referenced by:  breqtrri  4477  3brtr3i  4479  supsrlem  9509  0lt1  10100  hashunlei  12483  sqrt2gt1lt2  13108  trireciplem  13673  cos1bnd  13922  cos2bnd  13923  cos01gt0  13926  sin4lt0  13930  rpnnen2lem3  13950  gcdaddmlem  14166  dec2dvds  14549  abvtrivd  17489  sincos4thpi  22906  log2cnv  23275  log2ublem2  23278  log2ublem3  23279  birthday  23284  harmonicbnd3  23337  basellem7  23360  ppiublem1  23477  ppiublem2  23478  ppiub  23479  bposlem9  23567  lgsdir2lem2  23599  lgsdir2lem3  23600  ex-fl  25168  siilem1  25766  normlem5  26031  normlem6  26032  norm-ii-i  26054  norm3adifii  26065  cmm2i  26525  mayetes3i  26648  nmopcoadji  27020  mdoc2i  27345  dmdoc2i  27347  sqsscirc1  27890  log2le1  28023  ballotlem1c  28446  lgam1  28606  problem5  29023  circum  29040  cntotbnd  30292  jm2.23  30938  halffl  31493  wallispi  31852  stirlinglem1  31856  fouriersw  32014  bj-pinftyccb  34624  bj-minftyccb  34628

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