Theorem breqtri 5130

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  breqtrri  5132  3brtr3i  5134  supsrlem  11196  0lt1  11838  le9lt10  12846  9lt10  12951  hashunlei  14570  sqrt2gt1lt2  15441  trireciplem  16031  cos1bnd  16355  cos2bnd  16356  cos01gt0  16359  sin4lt0  16363  rpnnen2lem3  16384  z4even  16542  gcdaddmlem  16696  dec2dvds  17241  abvtrivd  21089  sincos4thpi  26842  log2cnv  27272  log2ublem2  27275  log2ublem3  27276  log2le1  27278  birthday  27282  harmonicbnd3  27335  lgam1  27391  basellem7  27414  ppiublem1  27529  ppiub  27531  bposlem4  27614  bposlem5  27615  bposlem9  27619  lgsdir2lem2  27653  lgsdir2lem3  27654  1reno  28883  ex-fl  31048  siilem1  31453  normlem5  31716  normlem6  31717  norm-ii-i  31739  norm3adifii  31750  cmm2i  32209  mayetes3i  32331  nmopcoadji  32703  mdoc2i  33028  dmdoc2i  33030  dp2lt10  33450  dp2ltsuc  33452  dplti  33471  sqsscirc1  34540  ballotlem1c  35140  hgt750lem  35280  problem5  36434  circum  36439  bj-pinftyccb  38142  bj-minftyccb  38146  poimirlem25  38563  cntotbnd  38730  3lexlogpow5ineq1  43104  3lexlogpow5ineq2  43105  aks4d1p1p2  43120  aks4d1p1p7  43124  posbezout  43150  aks6d1c7lem1  43230  jm2.23  44002  tr3dom  44528  halffl  46311  wallispi  47079  stirlinglem1  47083  fouriersw  47240  goldratval  47935