Theorem breqtri 4822

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 4805	. 2 ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑅𝐶)
4	1, 3	mpbi 221	1 ⊢ 𝐴𝑅𝐶

Syntax hints:   = wceq 1634   class class class wbr 4797

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754

This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-rab 3073  df-v 3357  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-nul 4074  df-if 4236  df-sn 4327  df-pr 4329  df-op 4333  df-br 4798

This theorem is referenced by:  breqtrri  4824  3brtr3i  4826  supsrlem  10155  0lt1  10773  le9lt10  11753  9lt10  11896  hashunlei  13436  sqrt2gt1lt2  14245  trireciplem  14823  cos1bnd  15145  cos2bnd  15146  cos01gt0  15149  sin4lt0  15153  rpnnen2lem3  15173  z4even  15338  gcdaddmlem  15474  dec2dvds  15994  abvtrivd  19070  sincos4thpi  24507  log2cnv  24913  log2ublem2  24916  log2ublem3  24917  log2le1  24919  birthday  24923  harmonicbnd3  24976  lgam1  25032  basellem7  25055  ppiublem1  25169  ppiublem2  25170  ppiub  25171  bposlem4  25254  bposlem5  25255  bposlem9  25259  lgsdir2lem2  25293  lgsdir2lem3  25294  ex-fl  27663  siilem1  28063  normlem5  28328  normlem6  28329  norm-ii-i  28351  norm3adifii  28362  cmm2i  28823  mayetes3i  28945  nmopcoadji  29317  mdoc2i  29642  dmdoc2i  29644  dp2lt10  29948  dp2ltsuc  29950  dplti  29970  sqsscirc1  30311  ballotlem1c  30926  hgt750lem  31086  problem5  31918  circum  31923  bj-pinftyccb  33462  bj-minftyccb  33466  poimirlem25  33784  cntotbnd  33943  jm2.23  38104  halffl  40035  wallispi  40810  stirlinglem1  40814  fouriersw  40971