Theorem sylan9eq 2796

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 597	1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1539

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780  df-cleq 2728

This theorem is referenced by:  sylan9req  2797  sylan9eqr  2798  difeq12  4058  uneq12  4098  ineq12  4147  ssdifim  4202  ifeq12  4483  ifbi  4487  ifeq12da  4498  preq12  4675  prprc  4707  opeq12  4811  eqsnuniex  5292  opthwiener  5441  opthhausdorff0  5445  xpeq12  5625  sosn  5684  nfimad  5988  coi2  6181  funprg  6517  funtpg  6518  funcnvtp  6526  funcnvqp  6527  funimass1  6545  fimadmfoALT  6729  f1orescnv  6761  resdif  6767  fvmpt2  6918  fvmptnf  6929  fveqressseq  6989  oveq12  7316  cbvmpov  7402  ovmpog  7464  fvmpopr2d  7466  caofinvl  7595  eqopi  7899  el2mpocsbcl  7957  fmpoco  7967  mposn  7975  fsuppeqg  8023  supp0cosupp0  8055  imacosupp  8056  mpocurryd  8116  fvmpocurryd  8118  wrecseq123OLD  8162  rdgsucmptf  8290  frsucmpt  8300  oevn0  8376  oa0r  8399  om1r  8405  oe1m  8407  omass  8442  oeoalem  8458  oeoa  8459  oeoe  8461  qseq12  8587  map0g  8703  xpcomco  8887  sbthlem4  8911  sbthlem5  8912  xpmapenlem  8969  phplem2  9029  phplem3OLD  9040  phplem4OLD  9041  unxpdomlem3  9073  funsnfsupp  9196  ordtypelem7  9327  ttrcltr  9518  cardennn  9785  dfac9  9938  alephsing  10078  axcc3  10240  ac6num  10281  konigthlem  10370  canthp1lem2  10455  ordpipq  10744  ltrnq  10781  addclprlem2  10819  mulclprlem  10821  prlem934  10835  prlem936  10849  mulcmpblnrlem  10872  addcnsr  10937  mulcnsr  10938  axcnre  10966  recex  11653  rpnnen1lem3  12765  rpnnen1lem5  12767  xaddpnf1  13006  xaddpnf2  13007  xaddmnf1  13008  xaddmnf2  13009  rexadd  13012  xnn0xaddcl  13015  xaddnemnf  13016  xaddnepnf  13017  xadddilem  13074  addmodlteq  13712  om2uzrani  13718  om2uzrdg  13722  seqf1olem2  13809  seqf1o  13810  modexp  13999  faclbnd4lem3  14055  hashunsng  14152  hashwrdn  14295  lsw1  14315  swrdfv  14406  swrdccat  14493  ccats1pfxeqbi  14500  revfv  14521  cshwsublen  14554  wrdlen2  14702  wrdl2exs2  14704  wwlktovf1  14717  relexp0  14779  relexpcnv  14791  shftcan1  14839  remul2  14886  immul2  14893  sumss  15481  geomulcvg  15633  fprodss  15703  binomfallfaclem2  15795  bpolylem  15803  ef0lem  15833  efieq1re  15953  rpnnen2lem1  15968  ruclem3  15987  dvdsnegb  16028  dvdscmul  16037  dvds2ln  16043  dvds2add  16044  dvds2sub  16045  gcdn0val  16250  rpmulgcd  16311  lcmn0val  16345  odzval  16537  pcval  16590  pcmpt  16638  prmreclem4  16665  1arithlem2  16670  vdwlem8  16734  ramcl2lem  16755  ramtcl  16756  ramtub  16758  ramcl2  16762  ramcl  16775  setsval  16913  prfcl  17965  curf1cl  17991  curfcl  17995  hofcl  18022  yonedalem4c  18040  psssdm  18345  grplactval  18722  mulgnn0gsum  18755  cntzval  18972  f1omvdco2  19101  pmtrfinv  19114  psgnunilem5  19147  odlem2  19192  gexlem2  19232  lsmvalx  19289  efgtval  19374  efgredlema  19391  vrgpval  19418  cyggex  19544  gsumcom2  19621  fincygsubgodd  19760  dvdsrtr  19939  abvtrivd  20145  lmhmco  20350  reslmhm  20359  lvecinv  20420  zrhmulg  20756  znzrhval  20799  ocvval  20917  mplmon2  21314  subrgasclcl  21320  coe1fv  21422  coe1fzgsumdlem  21517  evl1gsumdlem  21567  mat1dimscm  21669  dmatid  21689  scmatdmat  21709  mavmul0g  21747  1marepvmarrepid  21769  mdetunilem2  21807  gsummatr01lem3  21851  gsummatr01  21853  smadiadetlem3  21862  m2cpminvid2lem  21948  chpdmatlem2  22033  isopn3  22262  cnpval  22432  ptbasfi  22777  dfac14  22814  cnmptkk  22879  xkofvcn  22880  cnmptk1p  22881  cnmptk2  22882  xkocnv  23010  flfval  23186  ptcmplem3  23250  ptcmpg  23253  tmdmulg  23288  prdsxmslem2  23730  subgnm2  23835  nmoval  23924  fsum2cn  24079  pcovalg  24220  isclmp  24305  cphnm  24402  tcphnmval  24438  ovolctb  24699  ioorcl  24786  uniioombllem2  24792  itg1addlem3  24907  itg1climres  24924  itg2uba  24953  itg2splitlem  24958  elcpn  25143  dvexp  25162  dvexp2  25163  rolle  25199  cmvth  25200  mvth  25201  dvlip  25202  dvlipcn  25203  dvlip2  25204  dveq0  25209  dv11cn  25210  lhop1lem  25222  lhop2  25224  lhop  25225  dvcvx  25229  ftc2ditglem  25254  itgsubstlem  25257  ig1pval  25382  elply2  25402  coeid2  25445  coemul  25458  taylthlem2  25578  ulmdvlem1  25604  mtest  25608  pserval2  25615  abelthlem1  25635  abelthlem3  25637  abelthlem8  25643  abelthlem9  25644  pige3ALT  25721  0cxp  25866  leibpi  26137  igamgam  26243  mule1  26342  bposlem5  26481  lgsval3  26508  lgsdinn0  26538  dchrvmasumlem1  26688  dchrisum0flblem1  26701  rpvmasum2  26705  padicval  26810  axsegconlem1  27330  ax5seglem9  27350  axpasch  27354  axeuclidlem  27375  axcontlem2  27378  finsumvtxdg2ssteplem4  27960  usgr2wlkspthlem2  28171  crctcshlem4  28230  wwlknp  28253  wlkiswwlks2lem3  28281  wwlksnred  28302  wwlksnextproplem2  28320  umgrwwlks2on  28367  clwlkclwwlklem2a  28407  clwwisshclwwsn  28425  clwwlknlbonbgr1  28448  clwwlkn1loopb  28452  clwwlkf  28456  clwwlkext2edg  28465  wwlksext2clwwlk  28466  erclwwlknsym  28479  erclwwlkntr  28480  clwwlknon1  28506  clwwlknonex2  28518  eupth2lem3lem3  28639  eucrct2eupth  28654  fusgreghash2wspv  28744  2clwwlk2clwwlklem  28755  2clwwlk2clwwlk  28759  numclwwlk1lem2f1  28766  grpoidinvlem4  28914  grpoinvval  28930  grpodivval  28942  ipval  29110  sspgval  29136  sspsval  29138  sspnval  29144  nmooval  29170  ipasslem1  29238  ipasslem4  29241  hial0  29509  hial02  29510  ocsh  29690  pjhval  29804  hosval  30147  homval  30148  hodval  30149  hfsval  30150  hfmval  30151  braval  30351  kbval  30361  eigvalval  30367  0hmop  30390  adj0  30401  lnopeq0i  30414  nmopcoi  30502  pjclem4  30606  pj3si  30614  hstoh  30639  strlem3a  30659  hstrlem3a  30667  mdexchi  30742  atcv0eq  30786  atcv1  30787  fpwrelmap  31113  cycpmco2lem4  31441  cycpmco2lem5  31442  smatfval  31790  measxun2  32223  measdivcst  32237  measdivcstALTV  32238  ddeval1  32247  ddeval0  32248  ballotlemfp1  32503  signswmnd  32581  signstfvneq0  32596  signstfvc  32598  ftc2re  32623  itgexpif  32631  bnj1128  33015  subfacp1lem3  33189  subfacp1lem5  33191  cvmlift2lem3  33312  msubco  33538  altopthsn  34308  fnetr  34585  fnejoin2  34603  bj-evalid  35291  finxpreclem3  35608  finxpreclem5  35610  finxpreclem6  35611  curf  35799  curunc  35803  matunitlindf  35819  poimirlem4  35825  poimirlem25  35846  mblfinlem2  35859  mblfinlem3  35860  mbfresfi  35867  itg2addnclem  35872  itg2addnc  35875  ftc1anclem5  35898  isbnd3  35986  bndss  35988  grposnOLD  36084  ghomco  36093  xrneq12  36555  lkrval  37144  pmapval  37813  polvalN  37961  watvalN  38049  ldilset  38165  ltrnset  38174  dilsetN  38209  trnsetN  38212  trlset  38217  trlval  38218  cdleme16b  38335  cdleme31fv1  38447  cdlemg1idlemN  38628  tgrpset  38801  tendoset  38815  erngset  38856  erngplus  38859  erngmul  38862  erngset-rN  38864  erngplus-rN  38867  dvaset  39061  dvaplusg  39065  dvamulr  39068  dvavadd  39071  dvavsca  39073  diafval  39087  dvhset  39137  dvhmulr  39142  dvhvadd  39148  dvhvsca  39157  docafvalN  39178  djafvalN  39190  dibfval  39197  dicfval  39231  dihfval  39287  dihval  39288  dihvalc  39289  dihvalb  39293  dochfval  39406  djhfval  39453  lcdval  39645  mapdfval  39683  mapdn0  39725  hvmapfval  39815  hdmap1fval  39852  hdmapfval  39883  hgmapfval  39942  sn-it0e0  40434  pw2f1ocnv  40897  hbtlem7  40988  relexp0a  41362  ntrclscls00  41714  dvconstbi  41990  expgrowth  41991  addrfv  42125  subrfv  42126  mulvfv  42127  refsum2cnlem1  42618  limcperiod  43218  cncfiooiccre  43485  dvbdfbdioolem1  43518  itgioocnicc  43567  fourierdlem73  43769  fourierdlem82  43778  fourierdlem94  43790  fourierdlem103  43799  fourierdlem104  43800  fourierdlem113  43809  sqwvfoura  43818  etransclem46  43870  nnfoctbdjlem  44043  ovn0  44154  smflim  44365  afveu  44703  afv2eu  44788  fvmptrabdm  44843  imasetpreimafvbijlemfo  44915  lighneallem3  45117  mogoldbblem  45230  fpprel2  45251  sbgoldbwt  45287  nnsum4primeseven  45310  nnsum4primesevenALTV  45311  bgoldbtbnd  45319  lmod0rng  45484  rnghmval  45507  lmodvsmdi  45776  lincdifsn  45823  lcoel0  45827  islindeps2  45882  blenn0  45977  nn0sumshdiglemA  46023  itcoval0mpt  46070  rrx2plordisom  46127  aacllem  46563