Theorem breqtri 5149

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

Syntax hints:   = wceq 1540   class class class wbr 5124

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125

This theorem is referenced by:  breqtrri  5151  3brtr3i  5153  supsrlem  11130  0lt1  11764  le9lt10  12740  9lt10  12844  hashunlei  14448  sqrt2gt1lt2  15298  trireciplem  15883  cos1bnd  16210  cos2bnd  16211  cos01gt0  16214  sin4lt0  16218  rpnnen2lem3  16239  z4even  16396  gcdaddmlem  16548  dec2dvds  17088  abvtrivd  20797  sincos4thpi  26479  log2cnv  26911  log2ublem2  26914  log2ublem3  26915  log2le1  26917  birthday  26921  harmonicbnd3  26975  lgam1  27031  basellem7  27054  ppiublem1  27170  ppiub  27172  bposlem4  27255  bposlem5  27256  bposlem9  27260  lgsdir2lem2  27294  lgsdir2lem3  27295  0reno  28405  ex-fl  30433  siilem1  30837  normlem5  31100  normlem6  31101  norm-ii-i  31123  norm3adifii  31134  cmm2i  31593  mayetes3i  31715  nmopcoadji  32087  mdoc2i  32412  dmdoc2i  32414  dp2lt10  32863  dp2ltsuc  32865  dplti  32884  sqsscirc1  33944  ballotlem1c  34545  hgt750lem  34688  problem5  35696  circum  35701  bj-pinftyccb  37244  bj-minftyccb  37248  poimirlem25  37674  cntotbnd  37825  3lexlogpow5ineq1  42072  3lexlogpow5ineq2  42073  aks4d1p1p2  42088  aks4d1p1p7  42092  posbezout  42118  aks6d1c7lem1  42198  jm2.23  42995  tr3dom  43527  halffl  45305  wallispi  46079  stirlinglem1  46083  fouriersw  46240