Theorem eqbrtrdi 5187

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

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

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 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5149

This theorem is referenced by:  eqbrtrrdi  5188  domunsn  9152  mapdom1  9167  mapdom2  9173  pm54.43  10025  infmap2  10242  inar1  10799  gruina  10842  nn0ledivnn  13120  xltnegi  13228  leexp1a  14172  discr  14235  facwordi  14281  faclbnd3  14284  hashgt12el  14414  hashle2pr  14471  cnpart  15220  geomulcvg  15855  dvds1  16296  ramz2  16993  ramz  16994  gex1  19546  sylow2a  19574  en1top  22900  en2top  22901  hmph0  23712  ptcmplem2  23970  dscmet  24494  dscopn  24495  xrge0tsms2  24764  htpycc  24919  pcohtpylem  24959  pcopt  24962  pcopt2  24963  pcoass  24964  pcorevlem  24966  vitalilem5  25554  dvef  25925  dveq0  25946  dv11cn  25947  deg1lt0  26040  ply1rem  26113  fta1g  26117  plyremlem  26252  aalioulem3  26282  pige3ALT  26467  relogrn  26508  logneg  26535  cxpaddlelem  26699  mule1  27093  ppiub  27150  dchrabs2  27208  bposlem1  27230  zabsle1  27242  lgseisen  27325  lgsquadlem2  27327  rpvmasumlem  27433  qabvle  27571  ostth3  27584  precsexlem9  28126  nnsrecgt0d  28232  0reno  28238  colinearalg  28734  eengstr  28804  clwwlknon1le1  29924  eucrct2eupth  30068  nmosetn0  30588  nmoo0  30614  siii  30676  bcsiALT  31002  branmfn  31928  drngidlhash  33163  m1pmeq  33261  esumrnmpt2  33687  ballotlemrc  34150  pthhashvtx  34737  subfacval3  34799  sconnpi1  34849  fz0n  35325  poimirlem31  37124  itg2addnclem  37144  ftc1anc  37174  safesnsupfidom1o  42847  radcnvrat  43751  infxr  44749  stoweidlem18  45406  stoweidlem55  45443  fourierdlem62  45556  fourierswlem  45618  exple2lt6  47428  fvconstdomi  47912  f1omoALT  47914  indthincALT  48059

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

OSZAR »