Theorem breqtri 5191

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

Syntax hints:   = wceq 1537   class class class wbr 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167

This theorem is referenced by:  breqtrri  5193  3brtr3i  5195  supsrlem  11180  0lt1  11812  le9lt10  12785  9lt10  12889  hashunlei  14474  sqrt2gt1lt2  15323  trireciplem  15910  cos1bnd  16235  cos2bnd  16236  cos01gt0  16239  sin4lt0  16243  rpnnen2lem3  16264  z4even  16420  gcdaddmlem  16570  dec2dvds  17110  abvtrivd  20855  sincos4thpi  26573  log2cnv  27005  log2ublem2  27008  log2ublem3  27009  log2le1  27011  birthday  27015  harmonicbnd3  27069  lgam1  27125  basellem7  27148  ppiublem1  27264  ppiub  27266  bposlem4  27349  bposlem5  27350  bposlem9  27354  lgsdir2lem2  27388  lgsdir2lem3  27389  0reno  28447  ex-fl  30479  siilem1  30883  normlem5  31146  normlem6  31147  norm-ii-i  31169  norm3adifii  31180  cmm2i  31639  mayetes3i  31761  nmopcoadji  32133  mdoc2i  32458  dmdoc2i  32460  dp2lt10  32848  dp2ltsuc  32850  dplti  32869  sqsscirc1  33854  ballotlem1c  34472  hgt750lem  34628  problem5  35637  circum  35642  bj-pinftyccb  37187  bj-minftyccb  37191  poimirlem25  37605  cntotbnd  37756  3lexlogpow5ineq1  42011  3lexlogpow5ineq2  42012  aks4d1p1p2  42027  aks4d1p1p7  42031  posbezout  42057  aks6d1c7lem1  42137  jm2.23  42953  tr3dom  43490  halffl  45211  wallispi  45991  stirlinglem1  45995  fouriersw  46152