Theorem syl6reqr 2877

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

Ref	Expression
syl6reqr.1	⊢ (𝜑 → 𝐴 = 𝐵)
syl6reqr.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
syl6reqr	⊢ (𝜑 → 𝐶 = 𝐴)

Proof of Theorem syl6reqr

Step	Hyp	Ref	Expression
1		syl6reqr.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		syl6reqr.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2832	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	syl6req 2875	1 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816

This theorem is referenced by:  iftrue  4475  iffalse  4478  difprsn1  4735  dmmptg  6098  setlikespec  6171  funimacnv  6437  dmmptd  6495  resasplit  6550  dffv3  6668  dfimafn  6730  fniinfv  6744  dffv2  6758  fvco2  6760  fniunfv  7008  isoini  7093  zfrep6  7658  oprabco  7793  suppco  7872  oeeulem  8229  ixpconstg  8472  sbthlem4  8632  sbthlem5  8633  sbthlem6  8634  supval2  8921  hartogslem1  9008  cantnflem1d  9153  alephsuc2  9508  dfac3  9549  hsmexlem5  9854  axdc2lem  9872  gruima  10226  eqneg  11362  zeo  12071  fseq1p1m1  12984  hashfzo  13793  hashimarn  13804  wrdval  13867  wrdnval  13898  repswswrd  14148  s1co  14197  swrds2  14304  modfsummod  15151  telfsumo  15159  mulgcd  15898  algcvg  15922  phiprmpw  16115  phisum  16129  strfv3  16534  resslem  16559  pwssnf1o  16773  imassca  16794  homfeq  16966  oppcbas  16990  resscatc  17367  estrcbasbas  17383  funcestrcsetclem7  17398  funcestrcsetclem8  17399  funcestrcsetclem9  17400  fthestrcsetc  17402  fullestrcsetc  17403  equivestrcsetc  17404  setc1strwun  17405  funcsetcestrclem7  17413  funcsetcestrclem8  17414  funcsetcestrclem9  17415  fthsetcestrc  17417  fullsetcestrc  17418  lubsn  17706  ipotset  17769  ipole  17770  plusfeq  17862  pws0g  17949  frmd0  18027  efmndtset  18046  oppgplusfval  18478  gsmsymgrfix  18558  gsmsymgreq  18562  psgnunilem2  18625  sylow3lem2  18755  oppglsm  18769  frgpuplem  18900  frgpupf  18901  frgpup1  18903  frgpup3lem  18905  gsumzoppg  19066  ablfac1eu  19197  pgpfaclem1  19205  pwsmgp  19370  opprmulfval  19377  dfrhm2  19471  subrg1  19547  staffn  19622  issrngd  19634  scafeq  19656  lbsextlem4  19935  sralem  19951  sravsca  19956  sraip  19957  rnascl  20122  psrlinv  20179  opsrbaslem  20260  evlseu  20298  mpfsubrg  20318  ply1scl0  20460  evl1sca  20499  evls1var  20503  zlmlem  20666  zlmvsca  20671  znbaslem  20687  ipfeq  20796  ssipeq  20802  thlbas  20842  thlle  20843  thloc  20845  dsmmbase  20881  dsmmelbas  20885  frlmelbas  20902  frlmphl  20927  islindf4  20984  matbas  21024  matplusg  21025  matsca  21026  matvsca  21027  matbas2d  21034  matsubgcell  21045  matmulcell  21056  ofco2  21062  mattposm  21070  mat1f1o  21089  mdetunilem8  21230  madugsum  21254  cramerimplem2  21295  decpmatmullem  21381  paste  21904  ptpjcn  22221  uptx  22235  xpstopnlem1  22419  alexsubALTlem4  22660  cnextf  22676  submtmd  22714  ussval  22870  tuslem  22878  psmetge0  22924  xmetge0  22956  setsmsds  23088  sgrim  23242  tnglem  23251  tngtset  23260  tngngp2  23263  resubmet  23412  pcorev2  23634  om1plusg  23640  om1tset  23641  om1opn  23642  pi1grplem  23655  clmadd  23680  clmmul  23681  clmcj  23682  tcphtopn  23831  tchnmfval  23833  bcthlem1  23929  bcthlem2  23930  bcthlem4  23932  bcth3  23936  rrxmval  24010  rrxmfval  24011  rrxdsfi  24016  ehlbase  24020  minveclem3b  24033  pjthlem1  24042  volun  24148  voliun  24157  uniioovol  24182  itg2i1fseq  24358  itgcnlem  24392  iblabslem  24430  limcres  24486  cnplimc  24487  ply1termlem  24795  0dgr  24837  taylthlem1  24963  abelth  25031  lawcos  25396  lgambdd  25616  basellem8  25667  musum  25770  chtub  25790  dchrval  25812  dchrinvcl  25831  lgsval4lem  25886  lgsquadlem2  25959  m1lgs  25966  mirauto  26472  lmiisolem  26584  ttglem  26664  axlowdimlem16  26745  ebtwntg  26770  ecgrtg  26771  elntg2  26773  nbgrval  27120  uvtxupgrres  27192  clwlknf1oclwwlknlem3  27864  eucrct2eupth  28026  smcnlem  28476  siii  28632  pjhthlem1  29170  sbcies  30253  imadifxp  30353  dfimafnf  30383  funcnvmpt  30414  symgcom  30729  cycpmconjslem1  30798  rdivmuldivd  30864  resvlem  30906  qusker  30920  mdetpmtr12  31092  pstmval  31137  xpinpreima2  31152  pnfneige0  31196  zlmds  31207  zlmtset  31208  esumid  31305  esumrnmpt  31313  sxsigon  31453  carsgclctunlem1  31577  circlemethnat  31914  f1resfz0f1d  32363  pthhashvtx  32376  filnetlem4  33731  setsstrset  34430  finxpreclem4  34677  itg2addnclem  34945  iblabsnclem  34957  areacirc  34989  fnopabco  35000  heiborlem8  35098  rngoi  35179  drngoi  35231  ldualvsub  36293  dalemrotyz  36796  dalem6  36806  dalem7  36807  dalem11  36812  dalem12  36813  dalemrotps  36829  dalem30  36840  dalem35  36845  cdleme1  37365  cdleme9  37391  cdleme20c  37449  cdleme20d  37450  cdlemefrs29clN  37537  cdleme37m  37600  cdleme43aN  37627  cdlemg1b2  37709  cdlemg4f  37753  cdlemh2  37954  erngdvlem1  38126  erngdvlem2N  38127  erngdvlem3  38128  erngdvlem4  38129  erngdvlem1-rN  38134  erngdvlem2-rN  38135  erngdvlem3-rN  38136  erngdvlem4-rN  38137  dvh4dimN  38585  lcdvsub  38755  hlhilsca  39073  hlhilbase  39074  hlhilplus  39075  hlhilvsca  39085  hlhilip  39086  hlhilipval  39087  rnasclg  39138  uvcn0  39158  prjspeclsp  39269  mzpcompact2lem  39355  eldioph2lem1  39364  fiphp3d  39423  rmxypairf1o  39515  wopprc  39634  lmhmlnmsplit  39694  clcnvlem  39990  dmmptdf  41495  dmmptdf2  41510  ellimcabssub0  41905  cosknegpi  42157  fourierdlem58  42456  fourierdlem59  42457  fourierdlem72  42470  fourierdlem80  42478  sqwvfourb  42521  etransclem28  42554  etransclem41  42567  omef  42785  dfaimafn  43371  afv2co2  43463  sbgoldbo  43959  rrxlinesc  44729  rrxlinec  44730  rrx2linest2  44738  rrxsphere  44742  itsclinecirc0b  44768  itsclquadb  44770