Theorem breqtrrid 5101

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

Syntax hints:   → wi 4   = wceq 1536   class class class wbr 5063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-rab 3146  df-v 3495  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4465  df-sn 4565  df-pr 4567  df-op 4571  df-br 5064

This theorem is referenced by:  r1sdom  9200  alephordilem1  9496  mulge0  11155  xsubge0  12652  xmulgt0  12674  xmulge0  12675  xlemul1a  12679  sqlecan  13569  bernneq  13588  hashge1  13748  hashge2el2dif  13836  cnpart  14595  sqr0lem  14596  bitsfzo  15780  bitsmod  15781  bitsinv1lem  15786  pcge0  16194  prmreclem4  16251  prmreclem5  16252  isabvd  19587  abvtrivd  19607  isnzr2hash  20033  nmolb2d  23323  nmoi  23333  nmoleub  23336  nmo0  23340  ovolge0  24078  itg1ge0a  24308  fta1g  24759  plyrem  24892  taylfval  24945  abelthlem2  25018  sinq12ge0  25092  relogrn  25143  logneg  25169  cxpge0  25264  amgmlem  25565  bposlem5  25862  lgsdir2lem2  25900  2lgsoddprmlem3  25988  rpvmasumlem  26061  eupth2lem3lem3  28007  eupth2lemb  28014  blocnilem  28579  pjssge0ii  29457  unierri  29879  xlt2addrd  30482  locfinref  31129  esumcst  31346  ballotlem5  31781  poimirlem23  34953  poimirlem25  34955  poimirlem26  34956  poimirlem27  34957  poimirlem28  34958  itgaddnclem2  34989  pell14qrgt0  39531  monotoddzzfi  39614  rmxypos  39619  rmygeid  39636  stoweidlem18  42377  stoweidlem55  42414  wallispi2lem1  42430  fourierdlem62  42527  fourierdlem103  42568  fourierdlem104  42569  fourierswlem  42589  pgrpgt2nabl  44488  pw2m1lepw2m1  44649  amgmwlem  44977