Theorem breqtri 5133

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

This proof depends on syntax axioms:   = wceq 1569   class class class wbr 5106

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107

This theorem is used by:  breqtrri  5135  3brtr3i  5137  supsrlem  11209  0lt1  11851  le9lt10  12859  9lt10  12964  hashunlei  14583  sqrt2gt1lt2  15456  trireciplem  16046  cos1bnd  16370  cos2bnd  16371  cos01gt0  16374  sin4lt0  16378  rpnnen2lem3  16399  z4even  16557  gcdaddmlem  16711  dec2dvds  17256  abvtrivd  21104  sincos4thpi  26857  log2cnv  27287  log2ublem2  27290  log2ublem3  27291  log2le1  27293  birthday  27297  harmonicbnd3  27350  lgam1  27406  basellem7  27429  ppiublem1  27544  ppiub  27546  bposlem4  27629  bposlem5  27630  bposlem9  27634  lgsdir2lem2  27668  lgsdir2lem3  27669  1reno  28898  ex-fl  31063  siilem1  31468  normlem5  31731  normlem6  31732  norm-ii-i  31754  norm3adifii  31765  cmm2i  32224  mayetes3i  32346  nmopcoadji  32718  mdoc2i  33043  dmdoc2i  33045  dp2lt10  33506  dp2ltsuc  33508  dplti  33527  sqsscirc1  34596  ballotlem1c  35196  hgt750lem  35336  problem5  36558  circum  36563  bj-pinftyccb  38288  bj-minftyccb  38292  poimirlem25  38709  cntotbnd  38876  3lexlogpow5ineq1  43250  3lexlogpow5ineq2  43251  aks4d1p1p2  43266  aks4d1p1p7  43270  posbezout  43296  aks6d1c7lem1  43376  jm2.23  44149  tr3dom  44675  halffl  46457  wallispi  47225  stirlinglem1  47229  fouriersw  47386  goldratval  48081