Theorem breqtrrid 5104

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 2827	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	breqtrid 5103	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1537   class class class wbr 5066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067

This theorem is referenced by:  r1sdom  9203  alephordilem1  9499  mulge0  11158  xsubge0  12655  xmulgt0  12677  xmulge0  12678  xlemul1a  12682  sqlecan  13572  bernneq  13591  hashge1  13751  hashge2el2dif  13839  cnpart  14599  sqr0lem  14600  bitsfzo  15784  bitsmod  15785  bitsinv1lem  15790  pcge0  16198  prmreclem4  16255  prmreclem5  16256  isabvd  19591  abvtrivd  19611  isnzr2hash  20037  nmolb2d  23327  nmoi  23337  nmoleub  23340  nmo0  23344  ovolge0  24082  itg1ge0a  24312  fta1g  24761  plyrem  24894  taylfval  24947  abelthlem2  25020  sinq12ge0  25094  relogrn  25145  logneg  25171  cxpge0  25266  amgmlem  25567  bposlem5  25864  lgsdir2lem2  25902  2lgsoddprmlem3  25990  rpvmasumlem  26063  eupth2lem3lem3  28009  eupth2lemb  28016  blocnilem  28581  pjssge0ii  29459  unierri  29881  xlt2addrd  30482  locfinref  31105  esumcst  31322  ballotlem5  31757  poimirlem23  34930  poimirlem25  34932  poimirlem26  34933  poimirlem27  34934  poimirlem28  34935  itgaddnclem2  34966  pell14qrgt0  39505  monotoddzzfi  39588  rmxypos  39593  rmygeid  39610  stoweidlem18  42352  stoweidlem55  42389  wallispi2lem1  42405  fourierdlem62  42502  fourierdlem103  42543  fourierdlem104  42544  fourierswlem  42564  pgrpgt2nabl  44463  pw2m1lepw2m1  44624  amgmwlem  44952