Theorem sylan9eq 2785

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 2748	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶)
4	1, 2, 3	syl2an 594	1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717

This theorem is referenced by:  sylan9req  2786  sylan9eqr  2787  difeq12  4113  uneq12  4155  ineq12  4205  ssdifim  4261  ifeq12  4548  ifbi  4552  ifeq12da  4563  preq12  4741  prprc  4773  opeq12  4877  eqsnuniex  5361  opthwiener  5516  opthhausdorff0  5520  xpeq12  5703  sosn  5764  nfimad  6073  coi2  6269  funprg  6608  funtpg  6609  funcnvtp  6617  funcnvqp  6618  funimass1  6636  fimadmfoALT  6821  f1orescnv  6853  resdif  6859  fvmpt2  7015  fvmptnf  7026  fveqressseq  7088  oveq12  7428  cbvmpov  7515  ovmpog  7580  fvmpopr2d  7583  caofinvl  7716  eqopi  8030  el2mpocsbcl  8090  fmpoco  8100  mposn  8108  fsuppeqg  8181  supp0cosupp0  8214  imacosupp  8215  mpocurryd  8275  fvmpocurryd  8277  wrecseq123OLD  8321  rdgsucmptf  8449  frsucmpt  8459  oevn0  8536  oa0r  8559  om1r  8564  oe1m  8566  omass  8601  oeoalem  8617  oeoa  8618  oeoe  8620  qseq12  8785  map0g  8903  xpcomco  9087  sbthlem4  9111  sbthlem5  9112  xpmapenlem  9169  phplem2  9233  phplem3OLD  9244  phplem4OLD  9245  unxpdomlem3  9277  funsnfsupp  9417  ordtypelem7  9549  ttrcltr  9741  cardennn  10008  dfac9  10161  alephsing  10301  axcc3  10463  ac6num  10504  konigthlem  10593  canthp1lem2  10678  ordpipq  10967  ltrnq  11004  addclprlem2  11042  mulclprlem  11044  prlem934  11058  prlem936  11072  mulcmpblnrlem  11095  addcnsr  11160  mulcnsr  11161  axcnre  11189  recex  11878  rpnnen1lem3  12996  rpnnen1lem5  12998  xaddpnf1  13240  xaddpnf2  13241  xaddmnf1  13242  xaddmnf2  13243  rexadd  13246  xnn0xaddcl  13249  xaddnemnf  13250  xaddnepnf  13251  xadddilem  13308  addmodlteq  13947  om2uzrani  13953  om2uzrdg  13957  seqf1olem2  14043  seqf1o  14044  modexp  14236  faclbnd4lem3  14290  hashunsng  14387  hashwrdn  14533  lsw1  14553  swrdfv  14634  swrdccat  14721  ccats1pfxeqbi  14728  revfv  14749  cshwsublen  14782  wrdlen2  14931  wrdl2exs2  14933  wwlktovf1  14944  relexp0  15006  relexpcnv  15018  shftcan1  15066  remul2  15113  immul2  15120  sumss  15706  geomulcvg  15858  fprodss  15928  binomfallfaclem2  16020  bpolylem  16028  ef0lem  16058  efieq1re  16179  rpnnen2lem1  16194  ruclem3  16213  dvdsnegb  16254  dvdscmul  16263  dvds2ln  16269  dvds2add  16270  dvds2sub  16271  gcdn0val  16476  rpmulgcd  16535  lcmn0val  16569  odzval  16763  pcval  16816  pcmpt  16864  prmreclem4  16891  1arithlem2  16896  vdwlem8  16960  ramcl2lem  16981  ramtcl  16982  ramtub  16984  ramcl2  16988  ramcl  17001  setsval  17139  prfcl  18197  curf1cl  18223  curfcl  18227  hofcl  18254  yonedalem4c  18272  psssdm  18577  grplactval  19006  mulgnn0gsum  19043  cntzval  19284  f1omvdco2  19415  pmtrfinv  19428  psgnunilem5  19461  odlem2  19506  gexlem2  19549  lsmvalx  19606  efgtval  19690  efgredlema  19707  vrgpval  19734  cyggex  19865  gsumcom2  19942  fincygsubgodd  20081  dvdsrtr  20319  rnghmval  20391  abvtrivd  20732  lmhmco  20940  reslmhm  20949  lvecinv  21013  zrhmulg  21452  znzrhval  21497  ocvval  21616  mplmon2  22027  subrgasclcl  22033  coe1fv  22149  coe1fzgsumdlem  22247  evl1gsumdlem  22300  mat1dimscm  22421  dmatid  22441  scmatdmat  22461  mavmul0g  22499  1marepvmarrepid  22521  mdetunilem2  22559  gsummatr01lem3  22603  gsummatr01  22605  smadiadetlem3  22614  m2cpminvid2lem  22700  chpdmatlem2  22785  isopn3  23014  cnpval  23184  ptbasfi  23529  dfac14  23566  cnmptkk  23631  xkofvcn  23632  cnmptk1p  23633  cnmptk2  23634  xkocnv  23762  flfval  23938  ptcmplem3  24002  ptcmpg  24005  tmdmulg  24040  prdsxmslem2  24482  subgnm2  24587  nmoval  24676  fsum2cn  24833  pcovalg  24983  isclmp  25068  cphnm  25165  tcphnmval  25201  ovolctb  25463  ioorcl  25550  uniioombllem2  25556  itg1addlem3  25671  itg1climres  25688  itg2uba  25717  itg2splitlem  25722  elcpn  25908  dvexp  25929  dvexp2  25930  rolle  25966  cmvth  25967  cmvthOLD  25968  mvth  25969  dvlip  25970  dvlipcn  25971  dvlip2  25972  dveq0  25977  dv11cn  25978  lhop1lem  25990  lhop2  25992  lhop  25993  dvcvx  25997  ftc2ditglem  26024  itgsubstlem  26027  ig1pval  26155  elply2  26175  coeid2  26218  coemul  26231  taylthlem2  26354  taylthlem2OLD  26355  ulmdvlem1  26381  mtest  26385  pserval2  26392  abelthlem1  26413  abelthlem3  26415  abelthlem8  26421  abelthlem9  26422  pige3ALT  26499  0cxp  26645  leibpi  26919  igamgam  27026  mule1  27125  bposlem5  27266  lgsval3  27293  lgsdinn0  27323  dchrvmasumlem1  27473  dchrisum0flblem1  27486  rpvmasum2  27490  padicval  27595  abssid  28185  abssnid  28187  axsegconlem1  28800  ax5seglem9  28820  axpasch  28824  axeuclidlem  28845  axcontlem2  28848  finsumvtxdg2ssteplem4  29434  usgr2wlkspthlem2  29644  crctcshlem4  29703  wwlknp  29726  wlkiswwlks2lem3  29754  wwlksnred  29775  wwlksnextproplem2  29793  umgrwwlks2on  29840  clwlkclwwlklem2a  29880  clwwisshclwwsn  29898  clwwlknlbonbgr1  29921  clwwlkn1loopb  29925  clwwlkf  29929  clwwlkext2edg  29938  wwlksext2clwwlk  29939  erclwwlknsym  29952  erclwwlkntr  29953  clwwlknon1  29979  clwwlknonex2  29991  eupth2lem3lem3  30112  eucrct2eupth  30127  fusgreghash2wspv  30217  2clwwlk2clwwlklem  30228  2clwwlk2clwwlk  30232  numclwwlk1lem2f1  30239  grpoidinvlem4  30389  grpoinvval  30405  grpodivval  30417  ipval  30585  sspgval  30611  sspsval  30613  sspnval  30619  nmooval  30645  ipasslem1  30713  ipasslem4  30716  hial0  30984  hial02  30985  ocsh  31165  pjhval  31279  hosval  31622  homval  31623  hodval  31624  hfsval  31625  hfmval  31626  braval  31826  kbval  31836  eigvalval  31842  0hmop  31865  adj0  31876  lnopeq0i  31889  nmopcoi  31977  pjclem4  32081  pj3si  32089  hstoh  32114  strlem3a  32134  hstrlem3a  32142  mdexchi  32217  atcv0eq  32261  atcv1  32262  fpwrelmap  32597  cycpmco2lem4  32942  cycpmco2lem5  32943  smatfval  33527  measxun2  33960  measdivcst  33974  measdivcstALTV  33975  ddeval1  33984  ddeval0  33985  ballotlemfp1  34242  signswmnd  34320  signstfvneq0  34335  signstfvc  34337  ftc2re  34361  itgexpif  34369  bnj1128  34752  subfacp1lem3  34923  subfacp1lem5  34925  cvmlift2lem3  35046  msubco  35272  altopthsn  35688  fnetr  35966  fnejoin2  35984  bj-evalid  36686  finxpreclem3  37003  finxpreclem5  37005  finxpreclem6  37006  curf  37202  curunc  37206  matunitlindf  37222  poimirlem4  37228  poimirlem25  37249  mblfinlem2  37262  mblfinlem3  37263  mbfresfi  37270  itg2addnclem  37275  itg2addnc  37278  ftc1anclem5  37301  isbnd3  37388  bndss  37390  grposnOLD  37486  ghomco  37495  xrneq12  37985  lkrval  38690  pmapval  39360  polvalN  39508  watvalN  39596  ldilset  39712  ltrnset  39721  dilsetN  39756  trnsetN  39759  trlset  39764  trlval  39765  cdleme16b  39882  cdleme31fv1  39994  cdlemg1idlemN  40175  tgrpset  40348  tendoset  40362  erngset  40403  erngplus  40406  erngmul  40409  erngset-rN  40411  erngplus-rN  40414  dvaset  40608  dvaplusg  40612  dvamulr  40615  dvavadd  40618  dvavsca  40620  diafval  40634  dvhset  40684  dvhmulr  40689  dvhvadd  40695  dvhvsca  40704  docafvalN  40725  djafvalN  40737  dibfval  40744  dicfval  40778  dihfval  40834  dihval  40835  dihvalc  40836  dihvalb  40840  dochfval  40953  djhfval  41000  lcdval  41192  mapdfval  41230  mapdn0  41272  hvmapfval  41362  hdmap1fval  41399  hdmapfval  41430  hgmapfval  41489  fmpocos  41858  sn-it0e0  42105  zaddcomlem  42141  pw2f1ocnv  42600  hbtlem7  42691  relexp0a  43288  ntrclscls00  43638  dvconstbi  43913  expgrowth  43914  addrfv  44048  subrfv  44049  mulvfv  44050  refsum2cnlem1  44541  limcperiod  45154  cncfiooiccre  45421  dvbdfbdioolem1  45454  itgioocnicc  45503  fourierdlem73  45705  fourierdlem82  45714  fourierdlem94  45726  fourierdlem103  45735  fourierdlem104  45736  fourierdlem113  45745  sqwvfoura  45754  etransclem46  45806  nnfoctbdjlem  45981  ovn0  46092  smflim  46303  afveu  46671  afv2eu  46756  fvmptrabdm  46811  imasetpreimafvbijlemfo  46882  lighneallem3  47084  mogoldbblem  47197  fpprel2  47218  sbgoldbwt  47254  nnsum4primeseven  47277  nnsum4primesevenALTV  47278  bgoldbtbnd  47286  grimco  47364  lmod0rng  47477  lmodvsmdi  47632  lincdifsn  47678  lcoel0  47682  islindeps2  47737  blenn0  47832  nn0sumshdiglemA  47878  itcoval0mpt  47925  rrx2plordisom  47982  aacllem  48420