Theorem sylan9eq 2824

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  sylan9req  2825  sylan9eqr  2826  difeq12  4084  uneq12  4125  ineq12  4176  ssdifim  4234  ifeq12  4511  ifbi  4515  ifeq12da  4526  preq12  4706  prprc  4738  opeq12  4844  eqsnuniex  5333  opthwiener  5498  opthhausdorff0  5502  xpeq12  5687  sosn  5749  nfimad  6072  coi2  6266  funprg  6591  funtpg  6592  funcnvtp  6600  funcnvqp  6601  funimass1  6619  fimadmfoALT  6804  f1orescnv  6837  resdif  6843  fvmpt2  7002  fvmptnf  7013  fveqressseq  7075  oveq12  7420  cbvmpov  7506  ovmpog  7570  fvmpopr2d  7573  caofinvl  7707  eqopi  8021  el2mpocsbcl  8079  fmpoco  8089  mposn  8097  fsuppeqg  8171  supp0cosupp0  8203  imacosupp  8204  mpocurryd  8264  fvmpocurryd  8266  rdgsucmptf  8414  frsucmpt  8424  oevn0  8499  oa0r  8522  om1r  8527  oe1m  8529  omass  8564  oeoalem  8581  oeoa  8582  oeoe  8584  qseq12  8758  map0g  8881  xpcomco  9054  sbthlem4  9077  sbthlem5  9078  xpmapenlem  9131  phplem2  9188  unxpdomlem3  9217  funsnfsupp  9351  ordtypelem7  9485  ttrcltr  9684  cardennn  9968  dfac9  10119  alephsing  10259  axcc3  10421  ac6num  10462  konigthlem  10552  canthp1lem2  10637  ordpipq  10926  ltrnq  10963  addclprlem2  11001  mulclprlem  11003  prlem934  11017  prlem936  11031  mulcmpblnrlem  11054  addcnsr  11119  mulcnsr  11120  axcnre  11148  recex  11845  rpnnen1lem3  13002  rpnnen1lem5  13004  xaddpnf1  13251  xaddpnf2  13252  xaddmnf1  13253  xaddmnf2  13254  rexadd  13257  xnn0xaddcl  13260  xaddnemnf  13261  xaddnepnf  13262  xadddilem  13319  addmodlteq  13981  om2uzrani  13987  om2uzrdg  13991  seqf1olem2  14077  seqf1o  14078  modexp  14273  faclbnd4lem3  14330  hashunsng  14427  hashwrdn  14583  lsw1  14603  swrdfv  14685  swrdccat  14771  ccats1pfxeqbi  14778  revfv  14799  cshwsublen  14832  wrdlen2  14980  wrdl2exs2  14982  wwlktovf1  14993  relexp0  15059  relexpcnv  15071  shftcan1  15119  remul2  15180  immul2  15187  sumss  15774  geomulcvg  15929  fprodss  16001  binomfallfaclem2  16093  bpolylem  16101  ef0lem  16131  efieq1re  16254  rpnnen2lem1  16269  ruclem3  16288  dvdsnegb  16330  dvdscmul  16339  dvds2ln  16346  dvds2add  16347  dvds2sub  16348  gcdn0val  16555  rpmulgcd  16614  lcmn0val  16652  odzval  16850  pcval  16903  pcmpt  16951  prmreclem4  16978  1arithlem2  16983  vdwlem8  17047  ramcl2lem  17068  ramtcl  17069  ramtub  17071  ramcl2  17075  ramcl  17088  setsval  17226  prfcl  18258  curf1cl  18283  curfcl  18287  hofcl  18314  yonedalem4c  18332  psssdm  18637  chneq12  18669  grplactval  19107  mulgnn0gsum  19145  cntzval  19390  f1omvdco2  19517  pmtrfinv  19530  psgnunilem5  19563  odlem2  19608  gexlem2  19651  lsmvalx  19708  efgtval  19792  efgredlema  19809  vrgpval  19836  cyggex  19967  gsumcom2  20044  fincygsubgodd  20183  dvdsrtr  20449  rnghmval  20521  abvtrivd  20912  lmhmco  21141  reslmhm  21150  lvecinv  21214  zrhmulg  21627  znzrhval  21664  ocvval  21785  mplmon2  22180  subrgasclcl  22186  coe1fv  22334  coe1fzgsumdlem  22431  evl1gsumdlem  22484  mat1dimscm  22600  dmatid  22620  scmatdmat  22640  mavmul0g  22678  1marepvmarrepid  22700  mdetunilem2  22738  gsummatr01lem3  22782  gsummatr01  22784  smadiadetlem3  22793  m2cpminvid2lem  22879  chpdmatlem2  22964  isopn3  23191  cnpval  23361  ptbasfi  23706  dfac14  23743  cnmptkk  23808  xkofvcn  23809  cnmptk1p  23810  cnmptk2  23811  xkocnv  23939  flfval  24115  ptcmplem3  24179  ptcmpg  24182  tmdmulg  24217  prdsxmslem2  24654  subgnm2  24759  nmoval  24840  fsum2cn  24998  pcovalg  25139  isclmp  25224  cphnm  25320  tcphnmval  25356  ovolctb  25617  ioorcl  25704  uniioombllem2  25710  itg1addlem3  25825  itg1climres  25841  itg2uba  25870  itg2splitlem  25875  elcpn  26061  dvexp  26080  dvexp2  26081  rolle  26117  cmvth  26118  mvth  26119  dvlip  26120  dvlipcn  26121  dvlip2  26122  dveq0  26127  dv11cn  26128  lhop1lem  26140  lhop2  26142  lhop  26143  dvcvx  26147  ftc2ditglem  26172  itgsubstlem  26175  ig1pval  26301  elply2  26321  coeid2  26364  coemul  26377  taylthlem2  26502  ulmdvlem1  26528  mtest  26532  pserval2  26539  abelthlem1  26559  abelthlem3  26561  abelthlem8  26567  abelthlem9  26568  pige3ALT  26650  0cxp  26796  leibpi  27072  igamgam  27178  mule1  27277  bposlem5  27417  lgsval3  27444  lgsdinn0  27474  dchrvmasumlem1  27624  dchrisum0flblem1  27637  rpvmasum2  27641  padicval  27746  abssid  28399  abssnid  28401  axsegconlem1  29207  ax5seglem9  29227  axpasch  29231  axeuclidlem  29252  axcontlem2  29255  finsumvtxdg2ssteplem4  29838  usgr2wlkspthlem2  30047  crctcshlem4  30109  wwlknp  30132  wlkiswwlks2lem3  30160  wwlksnred  30181  wwlksnextproplem2  30199  usgrwwlks2on  30247  umgrwwlks2on  30248  clwlkclwwlklem2a  30289  clwwisshclwwsn  30307  clwwlknlbonbgr1  30330  clwwlkn1loopb  30334  clwwlkf  30338  clwwlkext2edg  30347  wwlksext2clwwlk  30348  erclwwlknsym  30361  erclwwlkntr  30362  clwwlknon1  30388  clwwlknonex2  30400  eupth2lem3lem3  30521  eucrct2eupth  30536  fusgreghash2wspv  30626  2clwwlk2clwwlklem  30637  2clwwlk2clwwlk  30641  numclwwlk1lem2f1  30648  grpoidinvlem4  30799  grpoinvval  30815  grpodivval  30827  ipval  30995  sspgval  31021  sspsval  31023  sspnval  31029  nmooval  31055  ipasslem1  31123  ipasslem4  31126  hial0  31394  hial02  31395  ocsh  31575  pjhval  31689  hosval  32032  homval  32033  hodval  32034  hfsval  32035  hfmval  32036  braval  32236  kbval  32246  eigvalval  32252  0hmop  32275  adj0  32286  lnopeq0i  32299  nmopcoi  32387  pjclem4  32491  pj3si  32499  hstoh  32524  strlem3a  32544  hstrlem3a  32552  mdexchi  32627  atcv0eq  32671  atcv1  32672  fpwrelmap  33018  cycpmco2lem4  33389  cycpmco2lem5  33390  fxpgaval  33427  smatfval  34129  measxun2  34544  measdivcst  34558  measdivcstALTV  34559  ddeval1  34568  ddeval0  34569  ballotlemfp1  34826  signswmnd  34888  signstfvneq0  34903  signstfvc  34905  ftc2re  34929  itgexpif  34937  bnj1128  35322  subfacp1lem3  35572  subfacp1lem5  35574  cvmlift2lem3  35695  msubco  35921  altopthsn  36351  ditgeq12d  36622  fnetr  36750  fnejoin2  36768  ttcsntrsucg  36921  bj-evalid  37605  finxpreclem3  37926  finxpreclem5  37928  finxpreclem6  37929  curf  38136  curunc  38140  matunitlindf  38156  poimirlem4  38162  poimirlem25  38183  mblfinlem2  38196  mblfinlem3  38197  mbfresfi  38204  itg2addnclem  38209  itg2addnc  38212  ftc1anclem5  38235  isbnd3  38322  bndss  38324  grposnOLD  38420  ghomco  38429  xrneq12  38940  lkrval  39751  pmapval  40420  polvalN  40568  watvalN  40656  ldilset  40772  ltrnset  40781  dilsetN  40816  trnsetN  40819  trlset  40824  trlval  40825  cdleme16b  40942  cdleme31fv1  41054  cdlemg1idlemN  41235  tgrpset  41408  tendoset  41422  erngset  41463  erngplus  41466  erngmul  41469  erngset-rN  41471  erngplus-rN  41474  dvaset  41668  dvaplusg  41672  dvamulr  41675  dvavadd  41678  dvavsca  41680  diafval  41694  dvhset  41744  dvhmulr  41749  dvhvadd  41755  dvhvsca  41764  docafvalN  41785  djafvalN  41797  dibfval  41804  dicfval  41838  dihfval  41894  dihval  41895  dihvalc  41896  dihvalb  41900  dochfval  42013  djhfval  42060  lcdval  42252  mapdfval  42290  mapdn0  42332  hvmapfval  42422  hdmap1fval  42459  hdmapfval  42490  hgmapfval  42549  fmpocos  42893  sn-it0e0  43066  zaddcomlem  43126  pw2f1ocnv  43655  hbtlem7  43743  relexp0a  44333  ntrclscls00  44683  dvconstbi  44935  expgrowth  44936  addrfv  45068  subrfv  45069  mulvfv  45070  refsum2cnlem1  45648  limcperiod  46235  cncfiooiccre  46500  dvbdfbdioolem1  46533  itgioocnicc  46582  fourierdlem73  46784  fourierdlem82  46793  fourierdlem94  46805  fourierdlem103  46814  fourierdlem104  46815  fourierdlem113  46824  sqwvfoura  46833  etransclem46  46885  nnfoctbdjlem  47060  ovn0  47171  smflim  47382  afveu  47778  afv2eu  47863  fvmptrabdm  47918  imasetpreimafvbijlemfo  48042  lighneallem3  48247  ppivalnnprm  48265  mogoldbblem  48373  fpprel2  48394  sbgoldbwt  48430  nnsum4primeseven  48453  nnsum4primesevenALTV  48454  bgoldbtbnd  48462  grimco  48542  cycl3grtri  48600  lmod0rng  48882  lmodvsmdi  49043  lincdifsn  49088  lcoel0  49092  islindeps2  49147  blenn0  49237  nn0sumshdiglemA  49283  itcoval0mpt  49330  rrx2plordisom  49387  nelsubclem  49729  aacllem  50474