Theorem sylan9eq 2790

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727

This theorem is referenced by:  sylan9req  2791  sylan9eqr  2792  difeq12  4096  uneq12  4138  ineq12  4190  ssdifim  4248  ifeq12  4519  ifbi  4523  ifeq12da  4534  preq12  4711  prprc  4743  opeq12  4851  eqsnuniex  5331  opthwiener  5489  opthhausdorff0  5493  xpeq12  5679  sosn  5741  nfimad  6056  coi2  6252  funprg  6589  funtpg  6590  funcnvtp  6598  funcnvqp  6599  funimass1  6617  fimadmfoALT  6800  f1orescnv  6832  resdif  6838  fvmpt2  6996  fvmptnf  7007  fveqressseq  7068  oveq12  7412  cbvmpov  7500  ovmpog  7564  fvmpopr2d  7567  caofinvl  7701  eqopi  8022  el2mpocsbcl  8082  fmpoco  8092  mposn  8100  fsuppeqg  8173  supp0cosupp0  8205  imacosupp  8206  mpocurryd  8266  fvmpocurryd  8268  wrecseq123OLD  8312  rdgsucmptf  8440  frsucmpt  8450  oevn0  8525  oa0r  8548  om1r  8553  oe1m  8555  omass  8590  oeoalem  8606  oeoa  8607  oeoe  8609  qseq12  8778  map0g  8896  xpcomco  9074  sbthlem4  9098  sbthlem5  9099  xpmapenlem  9156  phplem2  9217  phplem3OLD  9228  unxpdomlem3  9258  funsnfsupp  9402  ordtypelem7  9536  ttrcltr  9728  cardennn  9995  dfac9  10149  alephsing  10288  axcc3  10450  ac6num  10491  konigthlem  10580  canthp1lem2  10665  ordpipq  10954  ltrnq  10991  addclprlem2  11029  mulclprlem  11031  prlem934  11045  prlem936  11059  mulcmpblnrlem  11082  addcnsr  11147  mulcnsr  11148  axcnre  11176  recex  11867  rpnnen1lem3  12993  rpnnen1lem5  12995  xaddpnf1  13240  xaddpnf2  13241  xaddmnf1  13242  xaddmnf2  13243  rexadd  13246  xnn0xaddcl  13249  xaddnemnf  13250  xaddnepnf  13251  xadddilem  13308  addmodlteq  13962  om2uzrani  13968  om2uzrdg  13972  seqf1olem2  14058  seqf1o  14059  modexp  14254  faclbnd4lem3  14311  hashunsng  14408  hashwrdn  14563  lsw1  14583  swrdfv  14664  swrdccat  14751  ccats1pfxeqbi  14758  revfv  14779  cshwsublen  14812  wrdlen2  14961  wrdl2exs2  14963  wwlktovf1  14974  relexp0  15040  relexpcnv  15052  shftcan1  15100  remul2  15147  immul2  15154  sumss  15738  geomulcvg  15890  fprodss  15962  binomfallfaclem2  16054  bpolylem  16062  ef0lem  16092  efieq1re  16215  rpnnen2lem1  16230  ruclem3  16249  dvdsnegb  16291  dvdscmul  16300  dvds2ln  16306  dvds2add  16307  dvds2sub  16308  gcdn0val  16515  rpmulgcd  16574  lcmn0val  16612  odzval  16809  pcval  16862  pcmpt  16910  prmreclem4  16937  1arithlem2  16942  vdwlem8  17006  ramcl2lem  17027  ramtcl  17028  ramtub  17030  ramcl2  17034  ramcl  17047  setsval  17184  prfcl  18213  curf1cl  18238  curfcl  18242  hofcl  18269  yonedalem4c  18287  psssdm  18590  grplactval  19023  mulgnn0gsum  19061  cntzval  19302  f1omvdco2  19427  pmtrfinv  19440  psgnunilem5  19473  odlem2  19518  gexlem2  19561  lsmvalx  19618  efgtval  19702  efgredlema  19719  vrgpval  19746  cyggex  19877  gsumcom2  19954  fincygsubgodd  20093  dvdsrtr  20326  rnghmval  20398  abvtrivd  20790  lmhmco  20999  reslmhm  21008  lvecinv  21072  zrhmulg  21468  znzrhval  21505  ocvval  21625  mplmon2  22017  subrgasclcl  22023  coe1fv  22140  coe1fzgsumdlem  22239  evl1gsumdlem  22292  mat1dimscm  22411  dmatid  22431  scmatdmat  22451  mavmul0g  22489  1marepvmarrepid  22511  mdetunilem2  22549  gsummatr01lem3  22593  gsummatr01  22595  smadiadetlem3  22604  m2cpminvid2lem  22690  chpdmatlem2  22775  isopn3  23002  cnpval  23172  ptbasfi  23517  dfac14  23554  cnmptkk  23619  xkofvcn  23620  cnmptk1p  23621  cnmptk2  23622  xkocnv  23750  flfval  23926  ptcmplem3  23990  ptcmpg  23993  tmdmulg  24028  prdsxmslem2  24466  subgnm2  24571  nmoval  24652  fsum2cn  24811  pcovalg  24961  isclmp  25046  cphnm  25143  tcphnmval  25179  ovolctb  25441  ioorcl  25528  uniioombllem2  25534  itg1addlem3  25649  itg1climres  25665  itg2uba  25694  itg2splitlem  25699  elcpn  25886  dvexp  25907  dvexp2  25908  rolle  25944  cmvth  25945  cmvthOLD  25946  mvth  25947  dvlip  25948  dvlipcn  25949  dvlip2  25950  dveq0  25955  dv11cn  25956  lhop1lem  25968  lhop2  25970  lhop  25971  dvcvx  25975  ftc2ditglem  26002  itgsubstlem  26005  ig1pval  26131  elply2  26151  coeid2  26194  coemul  26207  taylthlem2  26332  taylthlem2OLD  26333  ulmdvlem1  26359  mtest  26363  pserval2  26370  abelthlem1  26391  abelthlem3  26393  abelthlem8  26399  abelthlem9  26400  pige3ALT  26479  0cxp  26625  leibpi  26902  igamgam  27009  mule1  27108  bposlem5  27249  lgsval3  27276  lgsdinn0  27306  dchrvmasumlem1  27456  dchrisum0flblem1  27469  rpvmasum2  27473  padicval  27578  abssid  28182  abssnid  28184  cutpw2  28334  axsegconlem1  28842  ax5seglem9  28862  axpasch  28866  axeuclidlem  28887  axcontlem2  28890  finsumvtxdg2ssteplem4  29474  usgr2wlkspthlem2  29686  crctcshlem4  29748  wwlknp  29771  wlkiswwlks2lem3  29799  wwlksnred  29820  wwlksnextproplem2  29838  umgrwwlks2on  29885  clwlkclwwlklem2a  29925  clwwisshclwwsn  29943  clwwlknlbonbgr1  29966  clwwlkn1loopb  29970  clwwlkf  29974  clwwlkext2edg  29983  wwlksext2clwwlk  29984  erclwwlknsym  29997  erclwwlkntr  29998  clwwlknon1  30024  clwwlknonex2  30036  eupth2lem3lem3  30157  eucrct2eupth  30172  fusgreghash2wspv  30262  2clwwlk2clwwlklem  30273  2clwwlk2clwwlk  30277  numclwwlk1lem2f1  30284  grpoidinvlem4  30434  grpoinvval  30450  grpodivval  30462  ipval  30630  sspgval  30656  sspsval  30658  sspnval  30664  nmooval  30690  ipasslem1  30758  ipasslem4  30761  hial0  31029  hial02  31030  ocsh  31210  pjhval  31324  hosval  31667  homval  31668  hodval  31669  hfsval  31670  hfmval  31671  braval  31871  kbval  31881  eigvalval  31887  0hmop  31910  adj0  31921  lnopeq0i  31934  nmopcoi  32022  pjclem4  32126  pj3si  32134  hstoh  32159  strlem3a  32179  hstrlem3a  32187  mdexchi  32262  atcv0eq  32306  atcv1  32307  fpwrelmap  32656  cycpmco2lem4  33086  cycpmco2lem5  33087  smatfval  33772  measxun2  34187  measdivcst  34201  measdivcstALTV  34202  ddeval1  34211  ddeval0  34212  ballotlemfp1  34470  signswmnd  34535  signstfvneq0  34550  signstfvc  34552  ftc2re  34576  itgexpif  34584  bnj1128  34967  subfacp1lem3  35150  subfacp1lem5  35152  cvmlift2lem3  35273  msubco  35499  altopthsn  35925  ditgeq12d  36186  fnetr  36315  fnejoin2  36333  bj-evalid  37040  finxpreclem3  37357  finxpreclem5  37359  finxpreclem6  37360  curf  37568  curunc  37572  matunitlindf  37588  poimirlem4  37594  poimirlem25  37615  mblfinlem2  37628  mblfinlem3  37629  mbfresfi  37636  itg2addnclem  37641  itg2addnc  37644  ftc1anclem5  37667  isbnd3  37754  bndss  37756  grposnOLD  37852  ghomco  37861  xrneq12  38347  lkrval  39052  pmapval  39722  polvalN  39870  watvalN  39958  ldilset  40074  ltrnset  40083  dilsetN  40118  trnsetN  40121  trlset  40126  trlval  40127  cdleme16b  40244  cdleme31fv1  40356  cdlemg1idlemN  40537  tgrpset  40710  tendoset  40724  erngset  40765  erngplus  40768  erngmul  40771  erngset-rN  40773  erngplus-rN  40776  dvaset  40970  dvaplusg  40974  dvamulr  40977  dvavadd  40980  dvavsca  40982  diafval  40996  dvhset  41046  dvhmulr  41051  dvhvadd  41057  dvhvsca  41066  docafvalN  41087  djafvalN  41099  dibfval  41106  dicfval  41140  dihfval  41196  dihval  41197  dihvalc  41198  dihvalb  41202  dochfval  41315  djhfval  41362  lcdval  41554  mapdfval  41592  mapdn0  41634  hvmapfval  41724  hdmap1fval  41761  hdmapfval  41792  hgmapfval  41851  fmpocos  42232  sn-it0e0  42405  zaddcomlem  42441  pw2f1ocnv  43008  hbtlem7  43096  relexp0a  43687  ntrclscls00  44037  dvconstbi  44306  expgrowth  44307  addrfv  44441  subrfv  44442  mulvfv  44443  refsum2cnlem1  45009  limcperiod  45605  cncfiooiccre  45872  dvbdfbdioolem1  45905  itgioocnicc  45954  fourierdlem73  46156  fourierdlem82  46165  fourierdlem94  46177  fourierdlem103  46186  fourierdlem104  46187  fourierdlem113  46196  sqwvfoura  46205  etransclem46  46257  nnfoctbdjlem  46432  ovn0  46543  smflim  46754  afveu  47130  afv2eu  47215  fvmptrabdm  47270  imasetpreimafvbijlemfo  47367  lighneallem3  47569  mogoldbblem  47682  fpprel2  47703  sbgoldbwt  47739  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  bgoldbtbnd  47771  grimco  47850  cycl3grtri  47907  lmod0rng  48152  lmodvsmdi  48302  lincdifsn  48348  lcoel0  48352  islindeps2  48407  blenn0  48501  nn0sumshdiglemA  48547  itcoval0mpt  48594  rrx2plordisom  48651  nelsubclem  48982  aacllem  49613