Theorem eqbrtrdi 5125

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

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087

This theorem is referenced by:  eqbrtrrdi  5126  domunsn  9059  mapdom1  9074  mapdom2  9080  pm54.43  9919  infmap2  10133  inar1  10692  gruina  10735  nn0ledivnn  13051  xltnegi  13162  leexp1a  14131  discr  14196  facwordi  14245  faclbnd3  14248  hashgt12el  14378  hashle2pr  14433  cnpart  15196  geomulcvg  15835  dvds1  16282  ramz2  16989  ramz  16990  gex1  19560  sylow2a  19588  en1top  22962  en2top  22963  hmph0  23773  ptcmplem2  24031  dscmet  24550  dscopn  24551  xrge0tsms2  24814  htpycc  24960  pcohtpylem  24999  pcopt  25002  pcopt2  25003  pcoass  25004  pcorevlem  25006  vitalilem5  25592  dvef  25960  dveq0  25980  dv11cn  25981  deg1lt0  26069  ply1rem  26144  fta1g  26148  plyremlem  26284  aalioulem3  26314  pige3ALT  26500  relogrn  26541  logneg  26568  cxpaddlelem  26731  mule1  27128  ppiub  27184  dchrabs2  27242  bposlem1  27264  zabsle1  27276  lgseisen  27359  lgsquadlem2  27361  rpvmasumlem  27467  qabvle  27605  ostth3  27618  precsexlem9  28224  nnsrecgt0d  28360  colinearalg  28996  eengstr  29066  clwwlknon1le1  30189  eucrct2eupth  30333  nmosetn0  30854  nmoo0  30880  siii  30942  bcsiALT  31268  branmfn  32194  fzo0opth  32894  drngidlhash  33512  m1pmeq  33663  cos9thpiminplylem1  33945  esumrnmpt2  34231  ballotlemrc  34694  pthhashvtx  35329  subfacval3  35390  sconnpi1  35440  fz0n  35932  poimirlem31  37989  itg2addnclem  38009  ftc1anc  38039  safesnsupfidom1o  43865  radcnvrat  44762  infxr  45817  stoweidlem18  46467  stoweidlem55  46504  fourierdlem62  46617  fourierswlem  46679  chnsubseqwl  47328  exple2lt6  48855  fvconstdomi  49382  f1omoALT  49385  indthincALT  49953