Theorem breqtrrid 5151

Description: A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)

Hypotheses

Ref	Expression
breqtrrid.1	⊢ 𝐴𝑅𝐵
breqtrrid.2	⊢ (𝜑 → 𝐶 = 𝐵)

Assertion

Ref	Expression
breqtrrid	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem breqtrrid

Step	Hyp	Ref	Expression
1		breqtrrid.1	. 2 ⊢ 𝐴𝑅𝐵
2		breqtrrid.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2775	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	breqtrid 5150	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1567   class class class wbr 5111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-br 5112

This theorem is referenced by:  r1sdom  9746  alephordilem1  10057  mulge0  11732  xsubge0  13287  xmulgt0  13309  xmulge0  13310  xlemul1a  13314  sqlecan  14245  bernneq  14265  hashge1  14425  hashge2el2dif  14517  cnpart  15291  sqrt0  15292  bitsfzo  16493  bitsmod  16494  bitsinv1lem  16499  pcge0  16922  prmreclem4  16979  prmreclem5  16980  isnzr2hash  20603  isabvd  20893  abvtrivd  20913  nmolb2d  24844  nmoi  24854  nmoleub  24857  nmo0  24861  ovolge0  25609  itg1ge0a  25839  fta1g  26296  plyrem  26435  taylfval  26488  abelthlem2  26561  sinq12ge0  26639  relogrn  26692  logneg  26719  cxpge0  26814  amgmlem  27120  bposlem5  27418  lgsdir2lem2  27456  2lgsoddprmlem3  27544  rpvmasumlem  27617  mulsge0d  28305  expsgt0  28596  eupth2lem3lem3  30522  eupth2lemb  30529  blocnilem  31097  pjssge0ii  31975  unierri  32397  xlt2addrd  33045  2sqr3minply  34115  locfinref  34176  esumcst  34398  ballotlem5  34835  poimirlem23  38217  poimirlem25  38219  poimirlem26  38220  poimirlem27  38221  poimirlem28  38222  itgaddnclem2  38253  sn-recgt0d  43176  pell14qrgt0  43513  monotoddzzfi  43596  rmxypos  43601  rmygeid  43618  stoweidlem18  46659  stoweidlem55  46696  wallispi2lem1  46712  fourierdlem62  46809  fourierdlem103  46850  fourierdlem104  46851  fourierswlem  46871  2ltceilhalf  47993  ceilhalfnn  48001  pgrpgt2nabl  49066  pw2m1lepw2m1  49220  amgmwlem  50511