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 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

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

This theorem is used by:  sylan9req  2816  sylan9eqr  2817  difeq12  4069  uneq12  4110  ineq12  4161  ssdifim  4219  ifeq12  4501  ifbi  4505  ifeq12da  4516  preq12  4696  prprc  4728  opeq12  4835  eqsnuniex  5326  opthwiener  5491  opthhausdorff0  5495  xpeq12  5680  sosn  5742  nfimad  6065  coi2  6260  funprg  6587  funtpg  6588  funcnvtp  6596  funcnvqp  6597  funimass1  6615  fimadmfoALT  6800  f1orescnv  6833  resdif  6839  fvmpt2  6998  fvmptnf  7009  fveqressseq  7072  oveq12  7422  cbvmpov  7508  ovmpog  7572  fvmpopr2d  7575  caofinvl  7710  eqopi  8022  el2mpocsbcl  8082  fmpoco  8092  mposn  8100  fsuppeqg  8174  supp0cosupp0  8206  imacosupp  8207  mpocurryd  8267  fvmpocurryd  8269  rdgsucmptf  8417  frsucmpt  8427  oevn0  8502  oa0r  8525  om1r  8530  oe1m  8532  omass  8567  oeoalem  8584  oeoa  8585  oeoe  8587  qseq12  8761  curf  8869  map0g  8891  xpcomco  9065  sbthlem4  9088  sbthlem5  9089  xpmapenlem  9142  phplem2  9199  unxpdomlem3  9228  funsnfsupp  9362  ordtypelem7  9496  ttrcltr  9695  cardennn  9988  dfac9  10139  alephsing  10278  axcc3  10440  ac6num  10481  konigthlem  10577  canthp1lem2  10662  ordpipq  10951  ltrnq  10988  addclprlem2  11026  mulclprlem  11028  prlem934  11042  prlem936  11056  mulcmpblnrlem  11079  addcnsr  11144  mulcnsr  11145  axcnre  11173  recex  11870  rpnnen1lem3  13029  rpnnen1lem5  13031  xaddpnf1  13278  xaddpnf2  13279  xaddmnf1  13280  xaddmnf2  13281  rexadd  13284  xnn0xaddcl  13287  xaddnemnf  13288  xaddnepnf  13289  xadddilem  13346  addmodlteq  14010  om2uzrani  14016  om2uzrdg  14020  seqf1olem2  14106  seqf1o  14107  modexp  14302  faclbnd4lem3  14359  hashunsng  14456  hashwrdn  14612  lsw1  14632  swrdfv  14716  swrdccat  14804  ccats1pfxeqbi  14811  revfv  14832  cshwsublen  14867  wrdlen2  15015  wrdl2exs2  15017  wwlktovf1  15030  relexp0  15096  relexpcnv  15108  shftcan1  15156  remul2  15217  immul2  15224  sumss  15810  geomulcvg  15965  fprodss  16035  binomfallfaclem2  16126  bpolylem  16134  ef0lem  16164  efieq1re  16287  rpnnen2lem1  16302  ruclem3  16321  dvdsnegb  16363  dvdscmul  16372  dvds2ln  16379  dvds2add  16380  dvds2sub  16381  gcdn0val  16588  rpmulgcd  16647  lcmn0val  16685  odzval  16883  pcval  16936  pcmpt  16984  prmreclem4  17011  1arithlem2  17016  vdwlem8  17080  ramcl2lem  17101  ramtcl  17102  ramtub  17104  ramcl2  17108  ramcl  17121  setsval  17259  prfcl  18291  curf1cl  18316  curfcl  18320  hofcl  18347  yonedalem4c  18365  psssdm  18670  chneq12  18702  grplactval  19165  mulgnn0gsum  19203  cntzval  19448  f1omvdco2  19575  pmtrfinv  19588  psgnunilem5  19621  odlem2  19666  gexlem2  19709  lsmvalx  19766  efgtval  19850  efgredlema  19867  vrgpval  19894  cyggex  20025  gsumcom2  20102  fincygsubgodd  20241  dvdsrtr  20509  rnghmval  20581  abvtrivd  20998  lmhmco  21227  reslmhm  21236  lvecinv  21300  zrhmulg  21722  znzrhval  21759  ocvval  21880  mplmon2  22277  subrgasclcl  22283  coe1fv  22431  coe1fzgsumdlem  22528  evl1gsumdlem  22581  mat1dimscm  22697  dmatid  22717  scmatdmat  22737  mavmul0g  22775  1marepvmarrepid  22797  mdetunilem2  22835  gsummatr01lem3  22879  gsummatr01  22881  smadiadetlem3  22890  matunitlindf  22903  m2cpminvid2lem  22979  chpdmatlem2  23064  isopn3  23291  cnpval  23461  ptbasfi  23807  dfac14  23844  cnmptkk  23909  xkofvcn  23910  cnmptk1p  23911  cnmptk2  23912  xkocnv  24040  flfval  24216  ptcmplem3  24280  ptcmpg  24283  tmdmulg  24318  prdsxmslem2  24755  subgnm2  24860  nmoval  24941  fsum2cn  25099  pcovalg  25240  isclmp  25325  cphnm  25421  tcphnmval  25457  ovolctb  25718  ioorcl  25805  uniioombllem2  25811  itg1addlem3  25926  itg1climres  25942  itg2uba  25971  itg2splitlem  25976  elcpn  26161  dvexp  26180  dvexp2  26181  rolle  26217  cmvth  26218  mvth  26219  dvlip  26220  dvlipcn  26221  dvlip2  26222  dveq0  26227  dv11cn  26228  lhop1lem  26240  lhop2  26242  lhop  26243  dvcvx  26247  ftc2ditglem  26272  itgsubstlem  26275  ig1pval  26401  elply2  26421  coeid2  26465  coemul  26478  taylthlem2  26610  ulmdvlem1  26636  mtest  26640  pserval2  26647  abelthlem1  26667  abelthlem3  26669  abelthlem8  26675  abelthlem9  26676  pige3ALT  26757  0cxp  26903  leibpi  27179  igamgam  27285  mule1  27384  bposlem5  27524  lgsval3  27551  lgsdinn0  27581  dchrvmasumlem1  27731  dchrisum0flblem1  27744  rpvmasum2  27748  padicval  27853  abssid  28506  abssnid  28508  axsegconlem1  29374  ax5seglem9  29394  axpasch  29398  axeuclidlem  29419  axcontlem2  29422  finsumvtxdg2ssteplem4  30008  usgr2wlkspthlem2  30223  crctcshlem4  30288  wwlknp  30311  wlkiswwlks2lem3  30339  wwlksnred  30360  wwlksnextproplem2  30378  usgrwwlks2on  30426  umgrwwlks2on  30427  clwlkclwwlklem2a  30468  clwwisshclwwsn  30486  clwwlknlbonbgr1  30509  clwwlkn1loopb  30513  clwwlkf  30517  clwwlkext2edg  30526  wwlksext2clwwlk  30527  erclwwlknsym  30540  erclwwlkntr  30541  clwwlknon1  30567  clwwlknonex2  30579  eupth2lem3lem3  30710  eucrct2eupth  30725  fusgreghash2wspv  30815  2clwwlk2clwwlklem  30826  2clwwlk2clwwlk  30830  numclwwlk1lem2f1  30837  grpoidinvlem4  30988  grpoinvval  31004  grpodivval  31016  ipval  31184  sspgval  31210  sspsval  31212  sspnval  31218  nmooval  31244  ipasslem1  31312  ipasslem4  31315  hial0  31583  hial02  31584  ocsh  31764  pjhval  31878  hosval  32221  homval  32222  hodval  32223  hfsval  32224  hfmval  32225  braval  32425  kbval  32435  eigvalval  32441  0hmop  32464  adj0  32475  lnopeq0i  32488  nmopcoi  32576  pjclem4  32680  pj3si  32688  hstoh  32713  strlem3a  32733  hstrlem3a  32741  mdexchi  32816  atcv0eq  32860  atcv1  32861  fpwrelmap  33204  cycpmco2lem4  33569  cycpmco2lem5  33570  fxpgaval  33607  smatfval  34305  measxun2  34721  measdivcst  34735  measdivcstALTV  34736  ddeval1  34745  ddeval0  34746  ballotlemfp1  35003  signswmnd  35065  signstfvneq0  35080  signstfvc  35082  ftc2re  35106  itgexpif  35114  bnj1128  35499  subfacp1lem3  35761  subfacp1lem5  35763  cvmlift2lem3  35884  msubco  36110  altopthsn  36541  ditgeq12d  36842  fnetr  36970  fnejoin2  36988  ttcsntrsucg  37141  bj-evalid  37826  finxpreclem3  38147  finxpreclem5  38149  finxpreclem6  38150  curunc  38356  poimirlem4  38373  poimirlem25  38394  mblfinlem2  38407  mblfinlem3  38408  mbfresfi  38415  itg2addnclem  38420  itg2addnc  38423  ftc1anclem5  38446  isbnd3  38534  bndss  38536  grposnOLD  38632  ghomco  38641  xrneq12  39150  lkrval  39961  pmapval  40630  polvalN  40778  watvalN  40866  ldilset  40982  ltrnset  40991  dilsetN  41026  trnsetN  41029  trlset  41034  trlval  41035  cdleme16b  41152  cdleme31fv1  41264  cdlemg1idlemN  41445  tgrpset  41618  tendoset  41632  erngset  41673  erngplus  41676  erngmul  41679  erngset-rN  41681  erngplus-rN  41684  dvaset  41878  dvaplusg  41882  dvamulr  41885  dvavadd  41888  dvavsca  41890  diafval  41904  dvhset  41954  dvhmulr  41959  dvhvadd  41965  dvhvsca  41974  docafvalN  41995  djafvalN  42007  dibfval  42014  dicfval  42048  dihfval  42104  dihval  42105  dihvalc  42106  dihvalb  42110  dochfval  42223  djhfval  42270  lcdval  42462  mapdfval  42500  mapdn0  42542  hvmapfval  42632  hdmap1fval  42669  hdmapfval  42700  hgmapfval  42759  fmpocos  43103  sn-it0e0  43291  zaddcomlem  43351  pw2f1ocnv  43878  hbtlem7  43966  relexp0a  44556  ntrclscls00  44906  dvconstbi  45158  expgrowth  45159  addrfv  45291  subrfv  45292  mulvfv  45293  refsum2cnlem1  45871  limcperiod  46458  cncfiooiccre  46723  dvbdfbdioolem1  46756  itgioocnicc  46805  fourierdlem73  47007  fourierdlem82  47016  fourierdlem94  47028  fourierdlem103  47037  fourierdlem104  47038  fourierdlem113  47047  sqwvfoura  47056  etransclem46  47108  nnfoctbdjlem  47283  ovn0  47394  smflim  47605  afveu  48041  afv2eu  48126  fvmptrabdm  48181  imasetpreimafvbijlemfo  48305  lighneallem3  48510  ppivalnnprm  48528  mogoldbblem  48636  fpprel2  48657  sbgoldbwt  48693  nnsum4primeseven  48716  nnsum4primesevenALTV  48717  bgoldbtbnd  48725  grimco  48805  cycl3grtri  48863  lmod0rng  49144  lmodvsmdi  49309  lincdifsn  49354  lcoel0  49358  islindeps2  49413  blenn0  49503  nn0sumshdiglemA  49549  itcoval0mpt  49596  rrx2plordisom  49653  nelsubclem  49993  aacllem  50772