Theorem eqbrtrdi 5124

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086

This theorem is referenced by:  eqbrtrrdi  5125  domunsn  9065  mapdom1  9080  mapdom2  9086  pm54.43  9925  infmap2  10139  inar1  10698  gruina  10741  nn0ledivnn  13057  xltnegi  13168  leexp1a  14137  discr  14202  facwordi  14251  faclbnd3  14254  hashgt12el  14384  hashle2pr  14439  cnpart  15202  geomulcvg  15841  dvds1  16288  ramz2  16995  ramz  16996  gex1  19566  sylow2a  19594  en1top  22949  en2top  22950  hmph0  23760  ptcmplem2  24018  dscmet  24537  dscopn  24538  xrge0tsms2  24801  htpycc  24947  pcohtpylem  24986  pcopt  24989  pcopt2  24990  pcoass  24991  pcorevlem  24993  vitalilem5  25579  dvef  25947  dveq0  25967  dv11cn  25968  deg1lt0  26056  ply1rem  26131  fta1g  26135  plyremlem  26270  aalioulem3  26300  pige3ALT  26484  relogrn  26525  logneg  26552  cxpaddlelem  26715  mule1  27111  ppiub  27167  dchrabs2  27225  bposlem1  27247  zabsle1  27259  lgseisen  27342  lgsquadlem2  27344  rpvmasumlem  27450  qabvle  27588  ostth3  27601  precsexlem9  28207  nnsrecgt0d  28343  colinearalg  28979  eengstr  29049  clwwlknon1le1  30171  eucrct2eupth  30315  nmosetn0  30836  nmoo0  30862  siii  30924  bcsiALT  31250  branmfn  32176  fzo0opth  32876  drngidlhash  33494  m1pmeq  33645  cos9thpiminplylem1  33926  esumrnmpt2  34212  ballotlemrc  34675  pthhashvtx  35310  subfacval3  35371  sconnpi1  35421  fz0n  35913  poimirlem31  37972  itg2addnclem  37992  ftc1anc  38022  safesnsupfidom1o  43844  radcnvrat  44741  infxr  45796  stoweidlem18  46446  stoweidlem55  46483  fourierdlem62  46596  fourierswlem  46658  chnsubseqwl  47309  exple2lt6  48840  fvconstdomi  49367  f1omoALT  49370  indthincALT  49938