Theorem eqbrtrdi 5131

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 5102	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
4	1, 3	mpbiri 258	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5092

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093

This theorem is referenced by:  eqbrtrrdi  5132  domunsn  9044  mapdom1  9059  mapdom2  9065  pm54.43  9897  infmap2  10111  inar1  10669  gruina  10712  nn0ledivnn  13008  xltnegi  13118  leexp1a  14082  discr  14147  facwordi  14196  faclbnd3  14199  hashgt12el  14329  hashle2pr  14384  cnpart  15147  geomulcvg  15783  dvds1  16230  ramz2  16936  ramz  16937  gex1  19470  sylow2a  19498  en1top  22869  en2top  22870  hmph0  23680  ptcmplem2  23938  dscmet  24458  dscopn  24459  xrge0tsms2  24722  htpycc  24877  pcohtpylem  24917  pcopt  24920  pcopt2  24921  pcoass  24922  pcorevlem  24924  vitalilem5  25511  dvef  25882  dveq0  25903  dv11cn  25904  deg1lt0  25994  ply1rem  26069  fta1g  26073  plyremlem  26210  aalioulem3  26240  pige3ALT  26427  relogrn  26468  logneg  26495  cxpaddlelem  26659  mule1  27056  ppiub  27113  dchrabs2  27171  bposlem1  27193  zabsle1  27205  lgseisen  27288  lgsquadlem2  27290  rpvmasumlem  27396  qabvle  27534  ostth3  27547  precsexlem9  28122  nnsrecgt0d  28248  0reno  28366  colinearalg  28855  eengstr  28925  clwwlknon1le1  30045  eucrct2eupth  30189  nmosetn0  30709  nmoo0  30735  siii  30797  bcsiALT  31123  branmfn  32049  fzo0opth  32748  drngidlhash  33371  m1pmeq  33519  cos9thpiminplylem1  33749  esumrnmpt2  34035  ballotlemrc  34499  pthhashvtx  35101  subfacval3  35162  sconnpi1  35212  fz0n  35704  poimirlem31  37631  itg2addnclem  37651  ftc1anc  37681  safesnsupfidom1o  43390  radcnvrat  44287  infxr  45346  stoweidlem18  45999  stoweidlem55  46036  fourierdlem62  46149  fourierswlem  46211  exple2lt6  48348  fvconstdomi  48876  f1omoALT  48879  indthincALT  49448