Theorem eqbrtrdi 5144

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 5113	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
4	1, 3	mpbiri 261	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:  eqbrtrrdi  5145  domunsn  9125  mapdom1  9140  mapdom2  9146  pm54.43  10006  infmap2  10219  inar1  10784  gruina  10827  nn0ledivnn  13157  xltnegi  13268  leexp1a  14239  discr  14304  facwordi  14353  faclbnd3  14356  hashgt12el  14487  hashle2pr  14542  cnpart  15327  geomulcvg  15965  dvds1  16409  ramz2  17116  ramz  17117  gex1  19718  sylow2a  19746  en1top  23209  en2top  23210  hmph0  24021  ptcmplem2  24279  dscmet  24798  dscopn  24799  xrge0tsms2  25062  htpycc  25208  pcohtpylem  25247  pcopt  25250  pcopt2  25251  pcoass  25252  pcorevlem  25254  vitalilem5  25840  dvef  26207  dveq0  26227  dv11cn  26228  deg1lt0  26316  ply1rem  26391  fta1g  26395  plyremlem  26534  aalioulem3  26570  pige3ALT  26757  relogrn  26798  logneg  26825  cxpaddlelem  26988  mule1  27384  ppiub  27440  dchrabs2  27498  bposlem1  27520  zabsle1  27532  lgseisen  27615  lgsquadlem2  27617  rpvmasumlem  27723  qabvle  27861  ostth3  27874  precsexlem9  28480  nnsrecgt0d  28616  colinearalg  29367  eengstr  29437  pthhashvtx  30194  clwwlknon1le1  30571  eucrct2eupth  30725  nmosetn0  31246  nmoo0  31272  siii  31334  bcsiALT  31660  branmfn  32586  fzo0opth  33274  drngidlhash  33861  fldlring  33909  m1pmeq  33995  cos9thpiminplylem1  34292  esumrnmpt2  34578  ballotlemrc  35042  subfacval3  35768  sconnpi1  35818  fz0n  36310  poimirlem31  38400  itg2addnclem  38420  ftc1anc  38450  safesnsupfidom1o  44257  radcnvrat  45138  infxr  46196  stoweidlem18  46846  stoweidlem55  46883  fourierdlem62  46996  fourierswlem  47058  chnsubseqwl  47707  exple2lt6  49294  fvconstdomi  49818  f1omoALT  49821  indthincALT  50389