Theorem sylan9eq 2794

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  sylan9req  2795  sylan9eqr  2796  difeq12  4052  uneq12  4093  ineq12  4144  ssdifim  4201  ifeq12  4473  ifbi  4477  ifeq12da  4488  preq12  4667  prprc  4699  opeq12  4806  eqsnuniex  5290  opthwiener  5455  opthhausdorff0  5459  xpeq12  5643  sosn  5705  nfimad  6021  coi2  6215  funprg  6539  funtpg  6540  funcnvtp  6548  funcnvqp  6549  funimass1  6567  fimadmfoALT  6750  f1orescnv  6782  resdif  6788  fvmpt2  6947  fvmptnf  6958  fveqressseq  7020  oveq12  7365  cbvmpov  7451  ovmpog  7515  fvmpopr2d  7518  caofinvl  7652  eqopi  7967  el2mpocsbcl  8024  fmpoco  8034  mposn  8042  fsuppeqg  8116  supp0cosupp0  8148  imacosupp  8149  mpocurryd  8209  fvmpocurryd  8211  rdgsucmptf  8357  frsucmpt  8367  oevn0  8440  oa0r  8463  om1r  8468  oe1m  8470  omass  8505  oeoalem  8522  oeoa  8523  oeoe  8525  qseq12  8698  map0g  8822  xpcomco  8995  sbthlem4  9018  sbthlem5  9019  xpmapenlem  9072  phplem2  9129  unxpdomlem3  9158  funsnfsupp  9295  ordtypelem7  9429  ttrcltr  9628  cardennn  9898  dfac9  10050  alephsing  10189  axcc3  10351  ac6num  10392  konigthlem  10482  canthp1lem2  10567  ordpipq  10856  ltrnq  10893  addclprlem2  10931  mulclprlem  10933  prlem934  10947  prlem936  10961  mulcmpblnrlem  10984  addcnsr  11049  mulcnsr  11050  axcnre  11078  recex  11773  rpnnen1lem3  12920  rpnnen1lem5  12922  xaddpnf1  13169  xaddpnf2  13170  xaddmnf1  13171  xaddmnf2  13172  rexadd  13175  xnn0xaddcl  13178  xaddnemnf  13179  xaddnepnf  13180  xadddilem  13237  addmodlteq  13899  om2uzrani  13905  om2uzrdg  13909  seqf1olem2  13995  seqf1o  13996  modexp  14191  faclbnd4lem3  14248  hashunsng  14345  hashwrdn  14500  lsw1  14520  swrdfv  14602  swrdccat  14688  ccats1pfxeqbi  14695  revfv  14716  cshwsublen  14749  wrdlen2  14897  wrdl2exs2  14899  wwlktovf1  14910  relexp0  14976  relexpcnv  14988  shftcan1  15036  remul2  15083  immul2  15090  sumss  15677  geomulcvg  15832  fprodss  15904  binomfallfaclem2  15996  bpolylem  16004  ef0lem  16034  efieq1re  16157  rpnnen2lem1  16172  ruclem3  16191  dvdsnegb  16233  dvdscmul  16242  dvds2ln  16249  dvds2add  16250  dvds2sub  16251  gcdn0val  16458  rpmulgcd  16517  lcmn0val  16555  odzval  16753  pcval  16806  pcmpt  16854  prmreclem4  16881  1arithlem2  16886  vdwlem8  16950  ramcl2lem  16971  ramtcl  16972  ramtub  16974  ramcl2  16978  ramcl  16991  setsval  17128  prfcl  18160  curf1cl  18185  curfcl  18189  hofcl  18216  yonedalem4c  18234  psssdm  18539  chneq12  18571  grplactval  19009  mulgnn0gsum  19047  cntzval  19287  f1omvdco2  19414  pmtrfinv  19427  psgnunilem5  19460  odlem2  19505  gexlem2  19548  lsmvalx  19605  efgtval  19689  efgredlema  19706  vrgpval  19733  cyggex  19864  gsumcom2  19941  fincygsubgodd  20080  dvdsrtr  20339  rnghmval  20411  abvtrivd  20804  lmhmco  21033  reslmhm  21042  lvecinv  21106  zrhmulg  21484  znzrhval  21521  ocvval  21642  mplmon2  22037  subrgasclcl  22043  coe1fv  22191  coe1fzgsumdlem  22289  evl1gsumdlem  22342  mat1dimscm  22458  dmatid  22478  scmatdmat  22498  mavmul0g  22536  1marepvmarrepid  22558  mdetunilem2  22596  gsummatr01lem3  22640  gsummatr01  22642  smadiadetlem3  22651  m2cpminvid2lem  22737  chpdmatlem2  22822  isopn3  23049  cnpval  23219  ptbasfi  23564  dfac14  23601  cnmptkk  23666  xkofvcn  23667  cnmptk1p  23668  cnmptk2  23669  xkocnv  23797  flfval  23973  ptcmplem3  24037  ptcmpg  24040  tmdmulg  24075  prdsxmslem2  24512  subgnm2  24617  nmoval  24698  fsum2cn  24856  pcovalg  24997  isclmp  25082  cphnm  25178  tcphnmval  25214  ovolctb  25475  ioorcl  25562  uniioombllem2  25568  itg1addlem3  25683  itg1climres  25699  itg2uba  25728  itg2splitlem  25733  elcpn  25919  dvexp  25938  dvexp2  25939  rolle  25975  cmvth  25976  mvth  25977  dvlip  25978  dvlipcn  25979  dvlip2  25980  dveq0  25985  dv11cn  25986  lhop1lem  25998  lhop2  26000  lhop  26001  dvcvx  26005  ftc2ditglem  26030  itgsubstlem  26033  ig1pval  26159  elply2  26179  coeid2  26222  coemul  26235  taylthlem2  26357  ulmdvlem1  26383  mtest  26387  pserval2  26394  abelthlem1  26414  abelthlem3  26416  abelthlem8  26422  abelthlem9  26423  pige3ALT  26502  0cxp  26648  leibpi  26924  igamgam  27030  mule1  27129  bposlem5  27269  lgsval3  27296  lgsdinn0  27326  dchrvmasumlem1  27476  dchrisum0flblem1  27489  rpvmasum2  27493  padicval  27598  abssid  28251  abssnid  28253  axsegconlem1  29004  ax5seglem9  29024  axpasch  29028  axeuclidlem  29049  axcontlem2  29052  finsumvtxdg2ssteplem4  29635  usgr2wlkspthlem2  29844  crctcshlem4  29906  wwlknp  29929  wlkiswwlks2lem3  29957  wwlksnred  29978  wwlksnextproplem2  29996  usgrwwlks2on  30044  umgrwwlks2on  30045  clwlkclwwlklem2a  30086  clwwisshclwwsn  30104  clwwlknlbonbgr1  30127  clwwlkn1loopb  30131  clwwlkf  30135  clwwlkext2edg  30144  wwlksext2clwwlk  30145  erclwwlknsym  30158  erclwwlkntr  30159  clwwlknon1  30185  clwwlknonex2  30197  eupth2lem3lem3  30318  eucrct2eupth  30333  fusgreghash2wspv  30423  2clwwlk2clwwlklem  30434  2clwwlk2clwwlk  30438  numclwwlk1lem2f1  30445  grpoidinvlem4  30596  grpoinvval  30612  grpodivval  30624  ipval  30792  sspgval  30818  sspsval  30820  sspnval  30826  nmooval  30852  ipasslem1  30920  ipasslem4  30923  hial0  31191  hial02  31192  ocsh  31372  pjhval  31486  hosval  31829  homval  31830  hodval  31831  hfsval  31832  hfmval  31833  braval  32033  kbval  32043  eigvalval  32049  0hmop  32072  adj0  32083  lnopeq0i  32096  nmopcoi  32184  pjclem4  32288  pj3si  32296  hstoh  32321  strlem3a  32341  hstrlem3a  32349  mdexchi  32424  atcv0eq  32468  atcv1  32469  fpwrelmap  32825  cycpmco2lem4  33210  cycpmco2lem5  33211  fxpgaval  33248  smatfval  33979  measxun2  34394  measdivcst  34408  measdivcstALTV  34409  ddeval1  34418  ddeval0  34419  ballotlemfp1  34676  signswmnd  34741  signstfvneq0  34756  signstfvc  34758  ftc2re  34782  itgexpif  34790  bnj1128  35172  subfacp1lem3  35410  subfacp1lem5  35412  cvmlift2lem3  35533  msubco  35759  altopthsn  36189  ditgeq12d  36450  fnetr  36579  fnejoin2  36597  ttcsntrsucg  36750  bj-evalid  37434  finxpreclem3  37755  finxpreclem5  37757  finxpreclem6  37758  curf  37965  curunc  37969  matunitlindf  37985  poimirlem4  37991  poimirlem25  38012  mblfinlem2  38025  mblfinlem3  38026  mbfresfi  38033  itg2addnclem  38038  itg2addnc  38041  ftc1anclem5  38064  isbnd3  38151  bndss  38153  grposnOLD  38249  ghomco  38258  xrneq12  38769  lkrval  39580  pmapval  40249  polvalN  40397  watvalN  40485  ldilset  40601  ltrnset  40610  dilsetN  40645  trnsetN  40648  trlset  40653  trlval  40654  cdleme16b  40771  cdleme31fv1  40883  cdlemg1idlemN  41064  tgrpset  41237  tendoset  41251  erngset  41292  erngplus  41295  erngmul  41298  erngset-rN  41300  erngplus-rN  41303  dvaset  41497  dvaplusg  41501  dvamulr  41504  dvavadd  41507  dvavsca  41509  diafval  41523  dvhset  41573  dvhmulr  41578  dvhvadd  41584  dvhvsca  41593  docafvalN  41614  djafvalN  41626  dibfval  41633  dicfval  41667  dihfval  41723  dihval  41724  dihvalc  41725  dihvalb  41729  dochfval  41842  djhfval  41889  lcdval  42081  mapdfval  42119  mapdn0  42161  hvmapfval  42251  hdmap1fval  42288  hdmapfval  42319  hgmapfval  42378  fmpocos  42720  sn-it0e0  42893  zaddcomlem  42953  pw2f1ocnv  43482  hbtlem7  43570  relexp0a  44160  ntrclscls00  44510  dvconstbi  44778  expgrowth  44779  addrfv  44912  subrfv  44913  mulvfv  44914  refsum2cnlem1  45485  limcperiod  46073  cncfiooiccre  46338  dvbdfbdioolem1  46371  itgioocnicc  46420  fourierdlem73  46622  fourierdlem82  46631  fourierdlem94  46643  fourierdlem103  46652  fourierdlem104  46653  fourierdlem113  46662  sqwvfoura  46671  etransclem46  46723  nnfoctbdjlem  46898  ovn0  47009  smflim  47220  afveu  47616  afv2eu  47701  fvmptrabdm  47756  imasetpreimafvbijlemfo  47880  lighneallem3  48085  ppivalnnprm  48103  mogoldbblem  48211  fpprel2  48232  sbgoldbwt  48268  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  bgoldbtbnd  48300  grimco  48380  cycl3grtri  48438  lmod0rng  48720  lmodvsmdi  48870  lincdifsn  48915  lcoel0  48919  islindeps2  48974  blenn0  49064  nn0sumshdiglemA  49110  itcoval0mpt  49157  rrx2plordisom  49214  nelsubclem  49557  aacllem  50291