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

Theorem breqtrrid 5142
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 2744 . 2 (𝜑𝐵 = 𝐶)
41, 3breqtrid 5141 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542   class class class wbr 5104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105
This theorem is referenced by:  r1sdom  9644  alephordilem1  9943  mulge0  11607  xsubge0  13109  xmulgt0  13131  xmulge0  13132  xlemul1a  13136  sqlecan  14039  bernneq  14058  hashge1  14217  hashge2el2dif  14307  cnpart  15059  sqr0lem  15060  bitsfzo  16250  bitsmod  16251  bitsinv1lem  16256  pcge0  16669  prmreclem4  16726  prmreclem5  16727  isabvd  20202  abvtrivd  20222  isnzr2hash  20657  nmolb2d  24004  nmoi  24014  nmoleub  24017  nmo0  24021  ovolge0  24767  itg1ge0a  24998  fta1g  25454  plyrem  25587  taylfval  25640  abelthlem2  25713  sinq12ge0  25787  relogrn  25839  logneg  25865  cxpge0  25960  amgmlem  26261  bposlem5  26558  lgsdir2lem2  26596  2lgsoddprmlem3  26684  rpvmasumlem  26757  eupth2lem3lem3  28960  eupth2lemb  28967  blocnilem  29532  pjssge0ii  30410  unierri  30832  xlt2addrd  31445  locfinref  32183  esumcst  32423  ballotlem5  32860  poimirlem23  35987  poimirlem25  35989  poimirlem26  35990  poimirlem27  35991  poimirlem28  35992  itgaddnclem2  36023  pell14qrgt0  41016  monotoddzzfi  41100  rmxypos  41105  rmygeid  41122  stoweidlem18  43969  stoweidlem55  44006  wallispi2lem1  44022  fourierdlem62  44119  fourierdlem103  44160  fourierdlem104  44161  fourierswlem  44181  pgrpgt2nabl  46142  pw2m1lepw2m1  46301  amgmwlem  46945
  Copyright terms: Public domain W3C validator