Theorem sylan9eq 2799

Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

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

Assertion

Ref	Expression
sylan9eq	⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)

Proof of Theorem sylan9eq

Step	Hyp	Ref	Expression
1		sylan9eq.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		sylan9eq.2	. 2 ⊢ (𝜓 → 𝐵 = 𝐶)
3		eqtr 2762	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶)
4	1, 2, 3	syl2an 595	1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-cleq 2731

This theorem is referenced by:  sylan9req  2800  sylan9eqr  2801  difeq12  4056  uneq12  4096  ineq12  4146  ssdifim  4201  ifeq12  4482  ifbi  4486  ifeq12da  4497  preq12  4676  prprc  4708  opeq12  4811  eqsnuniex  5286  opthwiener  5430  opthhausdorff0  5434  xpeq12  5613  sosn  5672  nfimad  5975  coi2  6164  funprg  6484  funtpg  6485  funcnvtp  6493  funcnvqp  6494  funimass1  6512  fimadmfoALT  6695  f1orescnv  6727  resdif  6732  fvmpt2  6880  fvmptnf  6891  fveqressseq  6951  oveq12  7277  cbvmpov  7361  ovmpog  7423  fvmpopr2d  7425  caofinvl  7554  eqopi  7853  el2mpocsbcl  7909  fmpoco  7919  mposn  7927  frnsuppeqg  7976  supp0cosupp0  8008  imacosupp  8009  mpocurryd  8069  fvmpocurryd  8071  wrecseq123OLD  8115  rdgsucmptf  8243  frsucmpt  8253  oevn0  8321  oa0r  8344  om1r  8350  oe1m  8352  omass  8387  oeoalem  8403  oeoa  8404  oeoe  8406  qseq12  8530  map0g  8646  xpcomco  8818  sbthlem4  8842  sbthlem5  8843  xpmapenlem  8896  phplem2  8955  phplem3OLD  8967  phplem4OLD  8968  unxpdomlem3  8990  funsnfsupp  9113  ordtypelem7  9244  ttrcltr  9435  cardennn  9725  dfac9  9876  alephsing  10016  axcc3  10178  ac6num  10219  konigthlem  10308  canthp1lem2  10393  ordpipq  10682  ltrnq  10719  addclprlem2  10757  mulclprlem  10759  prlem934  10773  prlem936  10787  mulcmpblnrlem  10810  addcnsr  10875  mulcnsr  10876  axcnre  10904  recex  11590  rpnnen1lem3  12701  rpnnen1lem5  12703  xaddpnf1  12942  xaddpnf2  12943  xaddmnf1  12944  xaddmnf2  12945  rexadd  12948  xnn0xaddcl  12951  xaddnemnf  12952  xaddnepnf  12953  xadddilem  13010  addmodlteq  13647  om2uzrani  13653  om2uzrdg  13657  seqf1olem2  13744  seqf1o  13745  modexp  13934  faclbnd4lem3  13990  hashunsng  14088  hashwrdn  14231  lsw1  14251  swrdfv  14342  swrdccat  14429  ccats1pfxeqbi  14436  revfv  14457  cshwsublen  14490  wrdlen2  14638  wrdl2exs2  14640  wwlktovf1  14653  relexp0  14715  relexpcnv  14727  shftcan1  14775  remul2  14822  immul2  14829  sumss  15417  geomulcvg  15569  fprodss  15639  binomfallfaclem2  15731  bpolylem  15739  ef0lem  15769  efieq1re  15889  rpnnen2lem1  15904  ruclem3  15923  dvdsnegb  15964  dvdscmul  15973  dvds2ln  15979  dvds2add  15980  dvds2sub  15981  gcdn0val  16186  rpmulgcd  16247  lcmn0val  16281  odzval  16473  pcval  16526  pcmpt  16574  prmreclem4  16601  1arithlem2  16606  vdwlem8  16670  ramcl2lem  16691  ramtcl  16692  ramtub  16694  ramcl2  16698  ramcl  16711  setsval  16849  prfcl  17901  curf1cl  17927  curfcl  17931  hofcl  17958  yonedalem4c  17976  psssdm  18281  grplactval  18658  mulgnn0gsum  18691  cntzval  18908  f1omvdco2  19037  pmtrfinv  19050  psgnunilem5  19083  odlem2  19128  gexlem2  19168  lsmvalx  19225  efgtval  19310  efgredlema  19327  vrgpval  19354  cyggex  19480  gsumcom2  19557  fincygsubgodd  19696  dvdsrtr  19875  abvtrivd  20081  lmhmco  20286  reslmhm  20295  lvecinv  20356  zrhmulg  20692  znzrhval  20735  ocvval  20853  mplmon2  21250  subrgasclcl  21256  coe1fv  21358  coe1fzgsumdlem  21453  evl1gsumdlem  21503  mat1dimscm  21605  dmatid  21625  scmatdmat  21645  mavmul0g  21683  1marepvmarrepid  21705  mdetunilem2  21743  gsummatr01lem3  21787  gsummatr01  21789  smadiadetlem3  21798  m2cpminvid2lem  21884  chpdmatlem2  21969  isopn3  22198  cnpval  22368  ptbasfi  22713  dfac14  22750  cnmptkk  22815  xkofvcn  22816  cnmptk1p  22817  cnmptk2  22818  xkocnv  22946  flfval  23122  ptcmplem3  23186  ptcmpg  23189  tmdmulg  23224  prdsxmslem2  23666  subgnm2  23771  nmoval  23860  fsum2cn  24015  pcovalg  24156  isclmp  24241  cphnm  24338  tcphnmval  24374  ovolctb  24635  ioorcl  24722  uniioombllem2  24728  itg1addlem3  24843  itg1climres  24860  itg2uba  24889  itg2splitlem  24894  elcpn  25079  dvexp  25098  dvexp2  25099  rolle  25135  cmvth  25136  mvth  25137  dvlip  25138  dvlipcn  25139  dvlip2  25140  dveq0  25145  dv11cn  25146  lhop1lem  25158  lhop2  25160  lhop  25161  dvcvx  25165  ftc2ditglem  25190  itgsubstlem  25193  ig1pval  25318  elply2  25338  coeid2  25381  coemul  25394  taylthlem2  25514  ulmdvlem1  25540  mtest  25544  pserval2  25551  abelthlem1  25571  abelthlem3  25573  abelthlem8  25579  abelthlem9  25580  pige3ALT  25657  0cxp  25802  leibpi  26073  igamgam  26179  mule1  26278  bposlem5  26417  lgsval3  26444  lgsdinn0  26474  dchrvmasumlem1  26624  dchrisum0flblem1  26637  rpvmasum2  26641  padicval  26746  axsegconlem1  27266  ax5seglem9  27286  axpasch  27290  axeuclidlem  27311  axcontlem2  27314  finsumvtxdg2ssteplem4  27896  usgr2wlkspthlem2  28105  crctcshlem4  28164  wwlknp  28187  wlkiswwlks2lem3  28215  wwlksnred  28236  wwlksnextproplem2  28254  umgrwwlks2on  28301  clwlkclwwlklem2a  28341  clwwisshclwwsn  28359  clwwlknlbonbgr1  28382  clwwlkn1loopb  28386  clwwlkf  28390  clwwlkext2edg  28399  wwlksext2clwwlk  28400  erclwwlknsym  28413  erclwwlkntr  28414  clwwlknon1  28440  clwwlknonex2  28452  eupth2lem3lem3  28573  eucrct2eupth  28588  fusgreghash2wspv  28678  2clwwlk2clwwlklem  28689  2clwwlk2clwwlk  28693  numclwwlk1lem2f1  28700  grpoidinvlem4  28848  grpoinvval  28864  grpodivval  28876  ipval  29044  sspgval  29070  sspsval  29072  sspnval  29078  nmooval  29104  ipasslem1  29172  ipasslem4  29175  hial0  29443  hial02  29444  ocsh  29624  pjhval  29738  hosval  30081  homval  30082  hodval  30083  hfsval  30084  hfmval  30085  braval  30285  kbval  30295  eigvalval  30301  0hmop  30324  adj0  30335  lnopeq0i  30348  nmopcoi  30436  pjclem4  30540  pj3si  30548  hstoh  30573  strlem3a  30593  hstrlem3a  30601  mdexchi  30676  atcv0eq  30720  atcv1  30721  fpwrelmap  31047  cycpmco2lem4  31375  cycpmco2lem5  31376  smatfval  31724  measxun2  32157  measdivcst  32171  measdivcstALTV  32172  ddeval1  32181  ddeval0  32182  ballotlemfp1  32437  signswmnd  32515  signstfvneq0  32530  signstfvc  32532  ftc2re  32557  itgexpif  32565  bnj1128  32949  subfacp1lem3  33123  subfacp1lem5  33125  cvmlift2lem3  33246  msubco  33472  altopthsn  34242  fnetr  34519  fnejoin2  34537  bj-evalid  35226  finxpreclem3  35543  finxpreclem5  35545  finxpreclem6  35546  curf  35734  curunc  35738  matunitlindf  35754  poimirlem4  35760  poimirlem25  35781  mblfinlem2  35794  mblfinlem3  35795  mbfresfi  35802  itg2addnclem  35807  itg2addnc  35810  ftc1anclem5  35833  isbnd3  35921  bndss  35923  grposnOLD  36019  ghomco  36028  xrneq12  36492  lkrval  37081  pmapval  37750  polvalN  37898  watvalN  37986  ldilset  38102  ltrnset  38111  dilsetN  38146  trnsetN  38149  trlset  38154  trlval  38155  cdleme16b  38272  cdleme31fv1  38384  cdlemg1idlemN  38565  tgrpset  38738  tendoset  38752  erngset  38793  erngplus  38796  erngmul  38799  erngset-rN  38801  erngplus-rN  38804  dvaset  38998  dvaplusg  39002  dvamulr  39005  dvavadd  39008  dvavsca  39010  diafval  39024  dvhset  39074  dvhmulr  39079  dvhvadd  39085  dvhvsca  39094  docafvalN  39115  djafvalN  39127  dibfval  39134  dicfval  39168  dihfval  39224  dihval  39225  dihvalc  39226  dihvalb  39230  dochfval  39343  djhfval  39390  lcdval  39582  mapdfval  39620  mapdn0  39662  hvmapfval  39752  hdmap1fval  39789  hdmapfval  39820  hgmapfval  39879  sn-it0e0  40377  pw2f1ocnv  40839  hbtlem7  40930  relexp0a  41277  ntrclscls00  41629  dvconstbi  41905  expgrowth  41906  addrfv  42040  subrfv  42041  mulvfv  42042  refsum2cnlem1  42533  limcperiod  43123  cncfiooiccre  43390  dvbdfbdioolem1  43423  itgioocnicc  43472  fourierdlem73  43674  fourierdlem82  43683  fourierdlem94  43695  fourierdlem103  43704  fourierdlem104  43705  fourierdlem113  43714  sqwvfoura  43723  etransclem46  43775  nnfoctbdjlem  43947  ovn0  44058  smflim  44263  afveu  44596  afv2eu  44681  fvmptrabdm  44736  imasetpreimafvbijlemfo  44809  lighneallem3  45011  mogoldbblem  45124  fpprel2  45145  sbgoldbwt  45181  nnsum4primeseven  45204  nnsum4primesevenALTV  45205  bgoldbtbnd  45213  lmod0rng  45378  rnghmval  45401  lmodvsmdi  45670  lincdifsn  45717  lcoel0  45721  islindeps2  45776  blenn0  45871  nn0sumshdiglemA  45917  itcoval0mpt  45964  rrx2plordisom  46021  aacllem  46457