MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  breqtrrid Structured version   Visualization version   GIF version

Theorem breqtrrid 5100
Description: A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
Hypotheses
Ref Expression
breqtrrid.1 𝐴𝑅𝐵
breqtrrid.2 (𝜑𝐶 = 𝐵)
Assertion
Ref Expression
breqtrrid (𝜑𝐴𝑅𝐶)

Proof of Theorem breqtrrid
StepHypRef Expression
1 breqtrrid.1 . 2 𝐴𝑅𝐵
2 breqtrrid.2 . . 3 (𝜑𝐶 = 𝐵)
32eqcomd 2831 . 2 (𝜑𝐵 = 𝐶)
41, 3breqtrid 5099 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530   class class class wbr 5062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-rab 3151  df-v 3501  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-br 5063
This theorem is referenced by:  r1sdom  9195  alephordilem1  9491  mulge0  11150  xsubge0  12647  xmulgt0  12669  xmulge0  12670  xlemul1a  12674  sqlecan  13564  bernneq  13583  hashge1  13743  hashge2el2dif  13831  cnpart  14592  sqr0lem  14593  bitsfzo  15776  bitsmod  15777  bitsinv1lem  15782  pcge0  16190  prmreclem4  16247  prmreclem5  16248  isabvd  19513  abvtrivd  19533  isnzr2hash  19958  nmolb2d  23242  nmoi  23252  nmoleub  23255  nmo0  23259  ovolge0  23997  itg1ge0a  24227  fta1g  24676  plyrem  24809  taylfval  24862  abelthlem2  24935  sinq12ge0  25009  relogrn  25058  logneg  25084  cxpge0  25179  amgmlem  25481  bposlem5  25778  lgsdir2lem2  25816  2lgsoddprmlem3  25904  rpvmasumlem  25977  eupth2lem3lem3  27923  eupth2lemb  27930  blocnilem  28495  pjssge0ii  29373  unierri  29795  xlt2addrd  30395  locfinref  30991  esumcst  31208  ballotlem5  31643  poimirlem23  34782  poimirlem25  34784  poimirlem26  34785  poimirlem27  34786  poimirlem28  34787  itgaddnclem2  34818  pell14qrgt0  39317  monotoddzzfi  39400  rmxypos  39405  rmygeid  39422  stoweidlem18  42165  stoweidlem55  42202  wallispi2lem1  42218  fourierdlem62  42315  fourierdlem103  42356  fourierdlem104  42357  fourierswlem  42377  pgrpgt2nabl  44242  pw2m1lepw2m1  44403  amgmwlem  44731
  Copyright terms: Public domain W3C validator