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

Theorem breqtrrid 5141
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 2743 . 2 (𝜑𝐵 = 𝐶)
41, 3breqtrid 5140 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541   class class class wbr 5103
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104
This theorem is referenced by:  r1sdom  9643  alephordilem1  9942  mulge0  11606  xsubge0  13108  xmulgt0  13130  xmulge0  13131  xlemul1a  13135  sqlecan  14038  bernneq  14057  hashge1  14216  hashge2el2dif  14306  cnpart  15058  sqr0lem  15059  bitsfzo  16249  bitsmod  16250  bitsinv1lem  16255  pcge0  16668  prmreclem4  16725  prmreclem5  16726  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  28972  eupth2lemb  28979  blocnilem  29544  pjssge0ii  30422  unierri  30844  xlt2addrd  31457  locfinref  32195  esumcst  32435  ballotlem5  32872  poimirlem23  35996  poimirlem25  35998  poimirlem26  35999  poimirlem27  36000  poimirlem28  36001  itgaddnclem2  36032  pell14qrgt0  41047  monotoddzzfi  41131  rmxypos  41136  rmygeid  41153  stoweidlem18  44012  stoweidlem55  44049  wallispi2lem1  44065  fourierdlem62  44162  fourierdlem103  44203  fourierdlem104  44204  fourierswlem  44224  pgrpgt2nabl  46191  pw2m1lepw2m1  46350  amgmwlem  46994
  Copyright terms: Public domain W3C validator