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

Theorem syl5eqbr 4720
Description: A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
Hypotheses
Ref Expression
syl5eqbr.1 𝐴 = 𝐵
syl5eqbr.2 (𝜑𝐵𝑅𝐶)
Assertion
Ref Expression
syl5eqbr (𝜑𝐴𝑅𝐶)

Proof of Theorem syl5eqbr
StepHypRef Expression
1 syl5eqbr.2 . 2 (𝜑𝐵𝑅𝐶)
2 syl5eqbr.1 . 2 𝐴 = 𝐵
3 eqid 2651 . 2 𝐶 = 𝐶
41, 2, 33brtr4g 4719 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523   class class class wbr 4685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686
This theorem is referenced by:  xp1en  8087  map2xp  8171  1sdom  8204  sucxpdom  8210  sniffsupp  8356  wdomima2g  8532  pwsdompw  9064  infunsdom1  9073  infunsdom  9074  infxp  9075  ackbij1lem5  9084  hsmexlem4  9289  imadomg  9394  unidom  9403  unictb  9435  pwcdandom  9527  distrnq  9821  supxrmnf  12185  xov1plusxeqvd  12356  quoremz  12694  quoremnn0ALT  12696  intfrac2  12697  m1modge3gt1  12757  bernneq2  13031  faclbnd4lem1  13120  sqrlem4  14030  reccn2  14371  caucvg  14453  o1fsum  14589  infcvgaux2i  14634  eirrlem  14976  rpnnen2lem12  14998  ruclem12  15014  nno  15145  divalglem5  15167  bitsfzolem  15203  bitsinv1lem  15210  bezoutlem3  15305  lcmfunsnlem  15401  coprmproddvds  15424  oddprmge3  15459  sqnprm  15461  prmreclem6  15672  4sqlem6  15694  4sqlem13  15708  4sqlem16  15711  4sqlem17  15712  2expltfac  15846  odcau  18065  sylow3  18094  efginvrel2  18186  lt6abl  18342  ablfac1lem  18513  evlslem2  19560  gzrngunitlem  19859  zringlpirlem3  19882  znfld  19957  chfacffsupp  20709  cpmidpmatlem3  20725  cctop  20858  csdfil  21745  xpsdsval  22233  nrginvrcnlem  22542  icccmplem2  22673  reconnlem2  22677  iscmet3lem3  23134  minveclem2  23243  minveclem4  23249  ivthlem2  23267  ivthlem3  23268  ovolunlem1a  23310  ovolfiniun  23315  ovoliunlem3  23318  ovoliun  23319  ovolicc2lem4  23334  unmbl  23351  ioombl1lem4  23375  itg2mono  23565  ibladdlem  23631  iblabsr  23641  iblmulc2  23642  dvferm1lem  23792  dvferm2lem  23794  lhop1lem  23821  dvcvx  23828  ftc1a  23845  plyeq0lem  24011  aannenlem3  24130  geolim3  24139  psercnlem1  24224  pserdvlem2  24227  reeff1olem  24245  pilem2  24251  pilem3  24252  cosq14gt0  24307  cosq14ge0  24308  cosne0  24321  recosf1o  24326  resinf1o  24327  argregt0  24401  logcnlem3  24435  logcnlem4  24436  logf1o2  24441  cxpcn3lem  24533  ang180lem2  24585  acosbnd  24672  atanbndlem  24697  leibpi  24714  cxp2lim  24748  emcllem2  24768  ftalem5  24848  basellem9  24860  vmage0  24892  chpge0  24897  chtub  24982  mersenne  24997  bposlem2  25055  bposlem5  25058  bposlem6  25059  bposlem9  25062  gausslemma2dlem0c  25128  gausslemma2dlem0e  25130  lgseisenlem1  25145  lgsquadlem1  25150  lgsquadlem2  25151  lgsquadlem3  25152  chebbnd1lem1  25203  chebbnd1lem2  25204  chebbnd1lem3  25205  mulog2sumlem2  25269  pntpbnd1a  25319  pntibndlem1  25323  pntibndlem3  25326  pntlemc  25329  ostth2  25371  ostth3  25372  pthdlem1  26718  smcnlem  27680  minvecolem2  27859  minvecolem4  27864  strlem5  29242  hstrlem5  29250  abrexdomjm  29471  prct  29620  dya2icoseg  30467  omssubadd  30490  omsmeas  30513  oddpwdc  30544  logdivsqrle  30856  faclim  31758  faclim2  31760  taupilem1  33297  mblfinlem3  33578  mblfinlem4  33579  ibladdnclem  33596  iblmulc2nc  33605  bddiblnc  33610  abrexdom  33655  dalem3  35268  dalem8  35274  dalem25  35302  dalem27  35303  dalem38  35314  dalem44  35320  dalem54  35330  lhpat3  35650  4atexlemunv  35670  4atexlemtlw  35671  4atexlemc  35673  4atexlemnclw  35674  4atexlemex2  35675  4atexlemcnd  35676  cdleme0b  35817  cdleme0c  35818  cdleme0fN  35823  cdlemeulpq  35825  cdleme01N  35826  cdleme0ex1N  35828  cdleme2  35833  cdleme3b  35834  cdleme3c  35835  cdleme3g  35839  cdleme3h  35840  cdleme4a  35844  cdleme7aa  35847  cdleme7c  35850  cdleme7d  35851  cdleme7e  35852  cdleme9  35858  cdleme11fN  35869  cdleme11k  35873  cdleme15d  35882  cdlemednpq  35904  cdleme19c  35910  cdleme20aN  35914  cdleme20e  35918  cdleme21c  35932  cdleme21ct  35934  cdleme22e  35949  cdleme22eALTN  35950  cdleme22f  35951  cdleme23a  35954  cdleme28a  35975  cdleme35f  36059  cdlemeg46frv  36130  cdlemeg46rgv  36133  cdlemeg46req  36134  cdlemg2fv2  36205  cdlemg2m  36209  cdlemg6c  36225  cdlemg31a  36302  cdlemg31b  36303  cdlemk10  36448  cdlemk37  36519  dia2dimlem1  36670  dihjatcclem4  37027  irrapxlem3  37705  pell14qrgapw  37757  dgrsub2  38022  radcnvrat  38830  ressiooinf  40102  fmul01  40130  fmul01lt1lem1  40134  fmul01lt1lem2  40135  sumnnodd  40180  climlimsupcex  40319  cnrefiisplem  40373  stoweidlem1  40536  stoweidlem5  40540  stoweidlem7  40542  dirkercncflem1  40638  dirkercncflem4  40641  fourierdlem30  40672  fourierdlem42  40684  fourierdlem48  40689  fourierdlem62  40703  fourierdlem63  40704  fourierdlem68  40709  fourierdlem79  40720  sqwvfoura  40763  etransclem32  40801  hoidmvlelem2  41131  iunhoiioolem  41210  vonioolem1  41215  pimdecfgtioo  41248  pimincfltioo  41249  smfmullem1  41319  fmtnoge3  41767  fmtnoprmfac2lem1  41803  sfprmdvdsmersenne  41845  lighneallem2  41848  lighneallem4a  41850  proththdlem  41855  stgoldbwt  41989  sgoldbeven3prm  41996  mogoldbb  41998  evengpop3  42011  bgoldbtbndlem2  42019  bgoldbtbndlem3  42020  lindslinindimp2lem3  42574  fllogbd  42679  nnolog2flm1  42709
  Copyright terms: Public domain W3C validator