Theorem breqtrrid 5143

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

This proof depends on syntax axioms:   → wi 4   = 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 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  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:  r1sdom  9756  alephordilem1  10109  mulge0  11789  xsubge0  13346  xmulgt0  13368  xmulge0  13369  xlemul1a  13373  sqlecan  14306  bernneq  14326  hashge1  14486  hashge2el2dif  14578  cnpart  15360  sqrt0  15361  bitsfzo  16558  bitsmod  16559  bitsinv1lem  16564  pcge0  16987  prmreclem4  17044  prmreclem5  17045  isnzr2hash  20717  isabvd  21016  abvtrivd  21036  nmolb2d  24984  nmoi  24994  nmoleub  24997  nmo0  25001  ovolge0  25749  itg1ge0a  25979  fta1g  26435  plyrem  26575  taylfval  26635  abelthlem2  26708  sinq12ge0  26786  relogrn  26838  logneg  26865  cxpge0  26960  amgmlem  27266  bposlem5  27564  lgsdir2lem2  27602  2lgsoddprmlem3  27690  rpvmasumlem  27763  mulsge0d  28451  expsgt0  28742  eupth2lem3lem3  30750  eupth2lemb  30757  blocnilem  31325  pjssge0ii  32203  unierri  32625  xlt2addrd  33270  2sqr3minply  34331  locfinref  34392  esumcst  34614  ballotlem5  35052  poimirlem23  38475  poimirlem25  38477  poimirlem26  38478  poimirlem27  38479  poimirlem28  38480  itgaddnclem2  38511  sn-recgt0d  43463  pell14qrgt0  43798  monotoddzzfi  43881  rmxypos  43886  rmygeid  43903  stoweidlem18  46944  stoweidlem55  46981  wallispi2lem1  46997  fourierdlem62  47094  fourierdlem103  47135  fourierdlem104  47136  fourierswlem  47156  2ltceilhalf  48318  ceilhalfnn  48326  pgrpgt2nabl  49394  pw2m1lepw2m1  49548  amgmwlem  50903