Theorem eqbrtrdi 5143

Description: A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.)

Hypotheses

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

Assertion

Ref	Expression
eqbrtrdi	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem eqbrtrdi

Step	Hyp	Ref	Expression
1		eqbrtrdi.2	. 2 ⊢ 𝐵𝑅𝐶
2		eqbrtrdi.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	breq1d 5112	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
4	1, 3	mpbiri 261	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103

This theorem is used by:  eqbrtrrdi  5144  domunsn  9153  mapdom1  9168  mapdom2  9174  pm54.43  10089  infmap2  10302  inar1  10867  gruina  10910  nn0ledivnn  13242  xltnegi  13353  leexp1a  14325  discr  14391  facwordi  14440  faclbnd3  14443  hashgt12el  14574  hashle2pr  14629  cnpart  15416  geomulcvg  16054  dvds1  16498  ramz2  17211  ramz  17212  gex1  19814  sylow2a  19842  en1top  23311  en2top  23312  hmph0  24123  ptcmplem2  24381  dscmet  24900  dscopn  24901  xrge0tsms2  25164  htpycc  25310  pcohtpylem  25349  pcopt  25352  pcopt2  25353  pcoass  25354  pcorevlem  25356  vitalilem5  25942  dvef  26309  dveq0  26329  dv11cn  26330  deg1lt0  26418  ply1rem  26493  fta1g  26497  plyremlem  26634  aalioulem3  26670  pige3ALT  26857  relogrn  26898  logneg  26925  cxpaddlelem  27088  mule1  27484  ppiub  27540  dchrabs2  27598  bposlem1  27620  zabsle1  27632  lgseisen  27715  lgsquadlem2  27717  rpvmasumlem  27823  qabvle  27961  ostth3  27974  precsexlem9  28610  nnsrecgt0d  28746  colinearalg  29497  eengstr  29567  pthhashvtx  30324  clwwlknon1le1  30701  eucrct2eupth  30855  nmosetn0  31376  nmoo0  31402  siii  31464  bcsiALT  31790  branmfn  32716  fzo0opth  33445  drngidlhash  34033  fldlring  34081  m1pmeq  34167  cos9thpiminplylem1  34464  esumrnmpt2  34750  ballotlemrc  35213  subfacval3  36044  sconnpi1  36094  fz0n  36592  poimirlem31  38678  itg2addnclem  38698  ftc1anc  38728  safesnsupfidom1o  44527  radcnvrat  45407  infxr  46486  stoweidlem18  47136  stoweidlem55  47173  fourierdlem62  47286  fourierswlem  47348  chnsubseqwl  47997  exple2lt6  49584  fvconstdomi  50114  f1omoALT  50117  indthincALT  50706