Theorem eqbrtrdi 5192

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

Syntax hints:   → wi 4   = wceq 1534   class class class wbr 5153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-br 5154

This theorem is referenced by:  eqbrtrrdi  5193  domunsn  9165  mapdom1  9180  mapdom2  9186  pm54.43  10044  infmap2  10261  inar1  10818  gruina  10861  nn0ledivnn  13141  xltnegi  13249  leexp1a  14194  discr  14257  facwordi  14306  faclbnd3  14309  hashgt12el  14439  hashle2pr  14496  cnpart  15245  geomulcvg  15880  dvds1  16321  ramz2  17026  ramz  17027  gex1  19589  sylow2a  19617  en1top  22978  en2top  22979  hmph0  23790  ptcmplem2  24048  dscmet  24572  dscopn  24573  xrge0tsms2  24842  htpycc  24997  pcohtpylem  25037  pcopt  25040  pcopt2  25041  pcoass  25042  pcorevlem  25044  vitalilem5  25632  dvef  26003  dveq0  26024  dv11cn  26025  deg1lt0  26118  ply1rem  26193  fta1g  26197  plyremlem  26332  aalioulem3  26362  pige3ALT  26547  relogrn  26588  logneg  26615  cxpaddlelem  26779  mule1  27176  ppiub  27233  dchrabs2  27291  bposlem1  27313  zabsle1  27325  lgseisen  27408  lgsquadlem2  27410  rpvmasumlem  27516  qabvle  27654  ostth3  27667  precsexlem9  28214  nnsrecgt0d  28322  0reno  28348  colinearalg  28844  eengstr  28914  clwwlknon1le1  30034  eucrct2eupth  30178  nmosetn0  30698  nmoo0  30724  siii  30786  bcsiALT  31112  branmfn  32038  fzo0opth  32707  drngidlhash  33309  m1pmeq  33455  esumrnmpt2  33901  ballotlemrc  34364  pthhashvtx  34955  subfacval3  35017  sconnpi1  35067  fz0n  35553  poimirlem31  37352  itg2addnclem  37372  ftc1anc  37402  safesnsupfidom1o  43084  radcnvrat  43988  infxr  44982  stoweidlem18  45639  stoweidlem55  45676  fourierdlem62  45789  fourierswlem  45851  exple2lt6  47743  fvconstdomi  48227  f1omoALT  48229  indthincALT  48374

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »