Theorem sylan9eq 2815

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  sylan9req  2816  sylan9eqr  2817  difeq12  4057  ineq12  4111  uneq12  4161  ssdifim  4217  ifeq12  4500  ifbi  4504  ifeq12da  4515  preq12  4692  prprc  4724  opeq12  4841  eqsnuniex  5323  opthwiener  5487  opthhausdorff0  5491  xpeq12  5676  sosn  5739  nfimad  6067  coi2  6268  funprg  6599  funtpg  6600  funcnvtp  6608  funcnvqp  6609  funimass1  6627  fimadmfoALT  6812  f1orescnv  6845  resdif  6851  fvmpt2  7010  fvmptnf  7021  fveqressseq  7084  oveq12  7433  cbvmpov  7519  ovmpog  7583  fvmpopr2d  7586  caofinvl  7729  eqopi  8041  el2mpocsbcl  8101  fmpoco  8112  mposn  8121  fsuppeqg  8201  supp0cosupp0  8233  imacosupp  8234  mpocurryd  8294  fvmpocurryd  8296  rdgsucmptf  8444  frsucmpt  8454  oevn0  8531  oa0r  8554  om1r  8559  oe1m  8561  omass  8596  oeoalem  8613  oeoa  8614  oeoe  8616  qseq12  8790  curf  8898  map0g  8920  xpcomco  9094  sbthlem4  9117  sbthlem5  9118  xpmapenlem  9171  phplem2  9228  unxpdomlem3  9257  funsnfsupp  9391  ordtypelem7  9525  ttrcltr  9724  cardennn  10071  dfac9  10222  alephsing  10361  axcc3  10523  ac6num  10564  konigthlem  10660  canthp1lem2  10745  ordpipq  11034  ltrnq  11071  addclprlem2  11109  mulclprlem  11111  prlem934  11125  prlem936  11139  mulcmpblnrlem  11162  addcnsr  11227  mulcnsr  11228  axcnre  11256  recex  11955  rpnnen1lem3  13114  rpnnen1lem5  13116  xaddpnf1  13363  xaddpnf2  13364  xaddmnf1  13365  xaddmnf2  13366  rexadd  13369  xnn0xaddcl  13372  xaddnemnf  13373  xaddnepnf  13374  xadddilem  13431  addmodlteq  14096  om2uzrani  14102  om2uzrdg  14106  seqf1olem2  14192  seqf1o  14193  modexp  14389  faclbnd4lem3  14446  hashunsng  14543  hashwrdn  14699  lsw1  14719  swrdfv  14804  swrdccat  14892  ccats1pfxeqbi  14899  revfv  14920  cshwsublen  14955  wrdlen2  15104  wrdl2exs2  15106  wwlktovf1  15119  relexp0  15185  relexpcnv  15197  shftcan1  15245  remul2  15306  immul2  15313  sumss  15899  geomulcvg  16054  fprodss  16124  binomfallfaclem2  16215  bpolylem  16223  ef0lem  16253  efieq1re  16376  rpnnen2lem1  16391  ruclem3  16410  dvdsnegb  16452  dvdscmul  16461  dvds2ln  16468  dvds2add  16469  dvds2sub  16470  gcdn0val  16677  rpmulgcd  16740  lcmn0val  16779  odzval  16978  pcval  17031  pcmpt  17079  prmreclem4  17106  1arithlem2  17111  vdwlem8  17175  ramcl2lem  17196  ramtcl  17197  ramtub  17199  ramcl2  17203  ramcl  17216  setsval  17354  prfcl  18386  curf1cl  18411  curfcl  18415  hofcl  18442  yonedalem4c  18460  psssdm  18765  chneq12  18797  grplactval  19261  mulgnn0gsum  19299  cntzval  19544  f1omvdco2  19671  pmtrfinv  19684  psgnunilem5  19717  odlem2  19762  gexlem2  19805  lsmvalx  19862  efgtval  19946  efgredlema  19963  vrgpval  19990  cyggex  20121  gsumcom2  20198  fincygsubgodd  20337  dvdsrtr  20607  rnghmval  20679  abvtrivd  21098  lmhmco  21327  reslmhm  21336  lvecinv  21400  zrhmulg  21824  znzrhval  21861  ocvval  21982  mplmon2  22379  subrgasclcl  22385  coe1fv  22533  coe1fzgsumdlem  22630  evl1gsumdlem  22683  mat1dimscm  22799  dmatid  22819  scmatdmat  22839  mavmul0g  22877  1marepvmarrepid  22899  mdetunilem2  22937  gsummatr01lem3  22981  gsummatr01  22983  smadiadetlem3  22992  matunitlindf  23005  m2cpminvid2lem  23081  chpdmatlem2  23166  isopn3  23393  cnpval  23563  ptbasfi  23909  dfac14  23946  cnmptkk  24011  xkofvcn  24012  cnmptk1p  24013  cnmptk2  24014  xkocnv  24142  flfval  24318  ptcmplem3  24382  ptcmpg  24385  tmdmulg  24420  prdsxmslem2  24857  subgnm2  24962  nmoval  25043  fsum2cn  25201  pcovalg  25342  isclmp  25427  cphnm  25523  tcphnmval  25559  ovolctb  25820  ioorcl  25907  uniioombllem2  25913  itg1addlem3  26028  itg1climres  26044  itg2uba  26073  itg2splitlem  26078  elcpn  26263  dvexp  26282  dvexp2  26283  rolle  26319  cmvth  26320  mvth  26321  dvlip  26322  dvlipcn  26323  dvlip2  26324  dveq0  26329  dv11cn  26330  lhop1lem  26342  lhop2  26344  lhop  26345  dvcvx  26349  ftc2ditglem  26374  itgsubstlem  26377  ig1pval  26503  elply2  26523  coeid2  26567  coemul  26580  taylthlem2  26710  ulmdvlem1  26736  mtest  26740  pserval2  26747  abelthlem1  26767  abelthlem3  26769  abelthlem8  26775  abelthlem9  26776  pige3ALT  26857  0cxp  27003  leibpi  27279  igamgam  27385  mule1  27484  bposlem5  27624  lgsval3  27651  lgsdinn0  27681  dchrvmasumlem1  27831  dchrisum0flblem1  27844  rpvmasum2  27848  padicval  27953  abssid  28636  abssnid  28638  axsegconlem1  29504  ax5seglem9  29524  axpasch  29528  axeuclidlem  29549  axcontlem2  29552  finsumvtxdg2ssteplem4  30138  usgr2wlkspthlem2  30353  crctcshlem4  30418  wwlknp  30441  wlkiswwlks2lem3  30469  wwlksnred  30490  wwlksnextproplem2  30508  usgrwwlks2on  30556  umgrwwlks2on  30557  clwlkclwwlklem2a  30598  clwwisshclwwsn  30616  clwwlknlbonbgr1  30639  clwwlkn1loopb  30643  clwwlkf  30647  clwwlkext2edg  30656  wwlksext2clwwlk  30657  erclwwlknsym  30670  erclwwlkntr  30671  clwwlknon1  30697  clwwlknonex2  30709  eupth2lem3lem3  30840  eucrct2eupth  30855  fusgreghash2wspv  30945  2clwwlk2clwwlklem  30956  2clwwlk2clwwlk  30960  numclwwlk1lem2f1  30967  grpoidinvlem4  31118  grpoinvval  31134  grpodivval  31146  ipval  31314  sspgval  31340  sspsval  31342  sspnval  31348  nmooval  31374  ipasslem1  31442  ipasslem4  31445  hial0  31713  hial02  31714  ocsh  31894  pjhval  32008  hosval  32351  homval  32352  hodval  32353  hfsval  32354  hfmval  32355  braval  32555  kbval  32565  eigvalval  32571  0hmop  32594  adj0  32605  lnopeq0i  32618  nmopcoi  32706  pjclem4  32810  pj3si  32818  hstoh  32843  strlem3a  32863  hstrlem3a  32871  mdexchi  32946  atcv0eq  32990  atcv1  32991  fpwrelmap  33375  cycpmco2lem4  33740  cycpmco2lem5  33741  fxpgaval  33778  smatfval  34477  measxun2  34893  measdivcst  34907  measdivcstALTV  34908  ddeval1  34917  ddeval0  34918  ballotlemfp1  35174  signswmnd  35236  signstfvneq0  35251  signstfvc  35253  ftc2re  35277  itgexpif  35285  bnj1128  35670  subfacp1lem3  36065  subfacp1lem5  36067  cvmlift2lem3  36188  msubco  36414  altopthsn  36850  ditgeq12d  37135  fnetr  37263  fnejoin2  37281  ttcsntrsucg  37434  bj-evalid  38133  finxpreclem3  38453  finxpreclem5  38455  finxpreclem6  38456  curunc  38662  poimirlem4  38679  poimirlem25  38700  mblfinlem2  38713  mblfinlem3  38714  mbfresfi  38721  itg2addnclem  38726  itg2addnc  38729  ftc1anclem5  38752  isbnd3  38855  bndss  38857  grposnOLD  38953  ghomco  38962  xrneq12  39471  lkrval  40282  pmapval  40951  polvalN  41099  watvalN  41187  ldilset  41303  ltrnset  41312  dilsetN  41347  trnsetN  41350  trlset  41355  trlval  41356  cdleme16b  41473  cdleme31fv1  41585  cdlemg1idlemN  41766  tgrpset  41939  tendoset  41953  erngset  41994  erngplus  41997  erngmul  42000  erngset-rN  42002  erngplus-rN  42005  dvaset  42199  dvaplusg  42203  dvamulr  42206  dvavadd  42209  dvavsca  42211  diafval  42225  dvhset  42275  dvhmulr  42280  dvhvadd  42286  dvhvsca  42295  docafvalN  42316  djafvalN  42328  dibfval  42335  dicfval  42369  dihfval  42425  dihval  42426  dihvalc  42427  dihvalb  42431  dochfval  42544  djhfval  42591  lcdval  42783  mapdfval  42821  mapdn0  42863  hvmapfval  42953  hdmap1fval  42990  hdmapfval  43021  hgmapfval  43080  fmpocos  43424  sn-it0e0  43604  zaddcomlem  43664  pw2f1ocnv  44181  hbtlem7  44264  relexp0a  44853  ntrclscls00  45203  dvconstbi  45455  expgrowth  45456  addrfv  45587  subrfv  45588  mulvfv  45589  refsum2cnlem1  46190  limcperiod  46776  cncfiooiccre  47041  dvbdfbdioolem1  47074  itgioocnicc  47123  fourierdlem73  47325  fourierdlem82  47334  fourierdlem94  47346  fourierdlem103  47355  fourierdlem104  47356  fourierdlem113  47365  sqwvfoura  47374  etransclem46  47426  nnfoctbdjlem  47601  ovn0  47712  smflim  47923  afveu  48359  afv2eu  48444  fvmptrabdm  48499  imasetpreimafvbijlemfo  48623  lighneallem3  48828  ppivalnnprm  48846  mogoldbblem  48954  fpprel2  48975  sbgoldbwt  49011  nnsum4primeseven  49034  nnsum4primesevenALTV  49035  bgoldbtbnd  49043  grimco  49123  cycl3grtri  49181  lmod0rng  49462  lmodvsmdi  49627  lincdifsn  49672  lcoel0  49676  islindeps2  49731  blenn0  49821  nn0sumshdiglemA  49867  itcoval0mpt  49914  rrx2plordisom  49972  nelsubclem  50317  aacllem  51150