Theorem breqtri 5136

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

This proof depends on syntax axioms:   = wceq 1570   class class class wbr 5109

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110

This theorem is used by:  breqtrri  5138  3brtr3i  5140  supsrlem  11100  0lt1  11740  le9lt10  12747  9lt10  12852  hashunlei  14467  sqrt2gt1lt2  15330  trireciplem  15921  cos1bnd  16247  cos2bnd  16248  cos01gt0  16251  sin4lt0  16255  rpnnen2lem3  16276  z4even  16434  gcdaddmlem  16586  dec2dvds  17127  abvtrivd  20944  sincos4thpi  26687  log2cnv  27118  log2ublem2  27121  log2ublem3  27122  log2le1  27124  birthday  27128  harmonicbnd3  27181  lgam1  27237  basellem7  27260  ppiublem1  27375  ppiub  27377  bposlem4  27460  bposlem5  27461  bposlem9  27465  lgsdir2lem2  27499  lgsdir2lem3  27500  1reno  28699  ex-fl  30807  siilem1  31212  normlem5  31475  normlem6  31476  norm-ii-i  31498  norm3adifii  31509  cmm2i  31968  mayetes3i  32090  nmopcoadji  32462  mdoc2i  32787  dmdoc2i  32789  dp2lt10  33212  dp2ltsuc  33214  dplti  33233  sqsscirc1  34307  ballotlem1c  34907  hgt750lem  35047  problem5  36169  circum  36174  bj-pinftyccb  37893  bj-minftyccb  37897  poimirlem25  38324  cntotbnd  38475  3lexlogpow5ineq1  42849  3lexlogpow5ineq2  42850  aks4d1p1p2  42865  aks4d1p1p7  42869  posbezout  42895  aks6d1c7lem1  42975  jm2.23  43751  tr3dom  44282  halffl  46043  wallispi  46812  stirlinglem1  46816  fouriersw  46973  sinnpoly  47656