Theorem sylan9eq 2818

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 2783	. 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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  sylan9req  2819  sylan9eqr  2820  difeq12  4061  ineq12  4115  uneq12  4165  ssdifim  4221  ifeq12  4504  ifbi  4508  ifeq12da  4519  preq12  4698  prprc  4730  opeq12  4847  eqsnuniex  5330  opthwiener  5494  opthhausdorff0  5498  xpeq12  5683  sosn  5746  nfimad  6083  coi2  6286  funprg  6624  funtpg  6625  funcnvtp  6633  funcnvqp  6634  funimass1  6652  fimadmfoALT  6837  f1orescnv  6870  resdif  6876  fvmpt2  7036  fvmptnf  7047  fveqressseq  7111  oveq12  7460  cbvmpov  7546  ovmpog  7611  fvmpopr2d  7614  caofinvl  7757  eqopi  8071  el2mpocsbcl  8131  fmpoco  8142  mposn  8151  fsuppeqg  8231  supp0cosupp0  8263  imacosupp  8264  mpocurryd  8324  fvmpocurryd  8326  rdgsucmptf  8474  frsucmpt  8484  oevn0  8561  oa0r  8584  om1r  8589  oe1m  8591  omass  8626  oeoalem  8643  oeoa  8644  oeoe  8646  qseq12  8820  curf  8928  map0g  8950  xpcomco  9124  sbthlem4  9147  sbthlem5  9148  xpmapenlem  9201  phplem2  9258  unxpdomlem3  9287  funsnfsupp  9421  ordtypelem7  9555  ttrcltr  9754  cardennn  10103  dfac9  10254  alephsing  10393  axcc3  10555  ac6num  10596  konigthlem  10692  canthp1lem2  10777  ordpipq  11066  ltrnq  11103  addclprlem2  11141  mulclprlem  11143  prlem934  11157  prlem936  11171  mulcmpblnrlem  11194  addcnsr  11259  mulcnsr  11260  axcnre  11288  recex  11988  rpnnen1lem3  13147  rpnnen1lem5  13149  xaddpnf1  13396  xaddpnf2  13397  xaddmnf1  13398  xaddmnf2  13399  rexadd  13402  xnn0xaddcl  13405  xaddnemnf  13406  xaddnepnf  13407  xadddilem  13464  addmodlteq  14129  om2uzrani  14135  om2uzrdg  14139  seqf1olem2  14225  seqf1o  14226  modexp  14423  faclbnd4lem3  14480  hashunsng  14577  hashwrdn  14733  lsw1  14753  swrdfv  14838  swrdccat  14926  ccats1pfxeqbi  14933  revfv  14954  cshwsublen  14989  wrdlen2  15138  wrdl2exs2  15140  wwlktovf1  15153  relexp0  15219  relexpcnv  15231  shftcan1  15279  remul2  15340  immul2  15347  sumss  15934  geomulcvg  16089  fprodss  16159  binomfallfaclem2  16250  bpolylem  16258  ef0lem  16288  efieq1re  16411  rpnnen2lem1  16426  ruclem3  16445  dvdsnegb  16487  dvdscmul  16496  dvds2ln  16503  dvds2add  16504  dvds2sub  16505  gcdn0val  16712  rpmulgcd  16775  lcmn0val  16814  odzval  17013  pcval  17066  pcmpt  17114  prmreclem4  17141  1arithlem2  17146  vdwlem8  17210  ramcl2lem  17231  ramtcl  17232  ramtub  17234  ramcl2  17238  ramcl  17251  setsval  17389  prfcl  18427  curf1cl  18452  curfcl  18456  hofcl  18483  yonedalem4c  18501  psssdm  18806  chneq12  18838  grplactval  19302  mulgnn0gsum  19340  cntzval  19586  f1omvdco2  19713  pmtrfinv  19726  psgnunilem5  19759  odlem2  19804  gexlem2  19847  lsmvalx  19904  efgtval  19988  efgredlema  20005  vrgpval  20032  cyggex  20163  gsumcom2  20240  fincygsubgodd  20379  dvdsrtr  20649  rnghmval  20721  abvtrivd  21140  lmhmco  21369  reslmhm  21378  lvecinv  21442  zrhmulg  21870  znzrhval  21907  ocvval  22028  mplmon2  22425  subrgasclcl  22431  coe1fv  22579  coe1fzgsumdlem  22676  evl1gsumdlem  22729  mat1dimscm  22845  dmatid  22865  scmatdmat  22885  mavmul0g  22923  1marepvmarrepid  22945  mdetunilem2  22983  gsummatr01lem3  23027  gsummatr01  23029  smadiadetlem3  23038  matunitlindf  23051  m2cpminvid2lem  23127  chpdmatlem2  23212  isopn3  23439  cnpval  23609  ptbasfi  23955  dfac14  23992  cnmptkk  24057  xkofvcn  24058  cnmptk1p  24059  cnmptk2  24060  xkocnv  24188  flfval  24364  ptcmplem3  24428  ptcmpg  24431  tmdmulg  24466  prdsxmslem2  24903  subgnm2  25008  nmoval  25089  fsum2cn  25247  pcovalg  25388  isclmp  25473  cphnm  25569  tcphnmval  25605  ovolctb  25866  ioorcl  25953  uniioombllem2  25959  itg1addlem3  26074  itg1climres  26090  itg2uba  26119  itg2splitlem  26124  elcpn  26309  dvexp  26328  dvexp2  26329  rolle  26365  cmvth  26366  mvth  26367  dvlip  26368  dvlipcn  26369  dvlip2  26370  dveq0  26375  dv11cn  26376  lhop1lem  26388  lhop2  26390  lhop  26391  dvcvx  26395  ftc2ditglem  26420  itgsubstlem  26423  ig1pval  26549  elply2  26569  coeid2  26613  coemul  26626  taylthlem2  26758  ulmdvlem1  26784  mtest  26788  pserval2  26795  abelthlem1  26815  abelthlem3  26817  abelthlem8  26823  abelthlem9  26824  pige3ALT  26905  0cxp  27051  leibpi  27327  igamgam  27433  mule1  27532  bposlem5  27672  lgsval3  27699  lgsdinn0  27729  dchrvmasumlem1  27879  dchrisum0flblem1  27892  rpvmasum2  27896  padicval  28001  abssid  28684  abssnid  28686  axsegconlem1  29552  ax5seglem9  29572  axpasch  29576  axeuclidlem  29597  axcontlem2  29600  finsumvtxdg2ssteplem4  30186  usgr2wlkspthlem2  30401  crctcshlem4  30466  wwlknp  30489  wlkiswwlks2lem3  30517  wwlksnred  30538  wwlksnextproplem2  30556  usgrwwlks2on  30604  umgrwwlks2on  30605  clwlkclwwlklem2a  30646  clwwisshclwwsn  30664  clwwlknlbonbgr1  30687  clwwlkn1loopb  30691  clwwlkf  30695  clwwlkext2edg  30704  wwlksext2clwwlk  30705  erclwwlknsym  30718  erclwwlkntr  30719  clwwlknon1  30745  clwwlknonex2  30757  eupth2lem3lem3  30888  eucrct2eupth  30903  fusgreghash2wspv  30993  2clwwlk2clwwlklem  31004  2clwwlk2clwwlk  31008  numclwwlk1lem2f1  31015  grpoidinvlem4  31166  grpoinvval  31182  grpodivval  31194  ipval  31362  sspgval  31388  sspsval  31390  sspnval  31396  nmooval  31422  ipasslem1  31490  ipasslem4  31493  hial0  31761  hial02  31762  ocsh  31942  pjhval  32056  hosval  32399  homval  32400  hodval  32401  hfsval  32402  hfmval  32403  braval  32603  kbval  32613  eigvalval  32619  0hmop  32642  adj0  32653  lnopeq0i  32666  nmopcoi  32754  pjclem4  32858  pj3si  32866  hstoh  32891  strlem3a  32911  hstrlem3a  32919  mdexchi  32994  atcv0eq  33038  atcv1  33039  fpwrelmap  33421  cycpmco2lem4  33789  cycpmco2lem5  33790  fxpgaval  33827  smatfval  34538  measxun2  34954  measdivcst  34968  measdivcstALTV  34969  ddeval1  34978  ddeval0  34979  ballotlemfp1  35235  signswmnd  35297  signstfvneq0  35312  signstfvc  35314  ftc2re  35338  itgexpif  35346  bnj1128  35731  subfacp1lem3  36155  subfacp1lem5  36157  cvmlift2lem3  36278  msubco  36504  altopthsn  36941  ditgeq12d  37226  fnetr  37354  fnejoin2  37372  ttcsntrsucg  37525  bj-evalid  38267  finxpreclem3  38584  finxpreclem5  38586  finxpreclem6  38587  curunc  38793  poimirlem4  38810  poimirlem25  38831  mblfinlem2  38844  mblfinlem3  38845  mbfresfi  38852  itg2addnclem  38857  itg2addnc  38860  ftc1anclem5  38883  isbnd3  38984  bndss  38986  grposnOLD  39082  ghomco  39091  xrneq12  39600  lkrval  40411  pmapval  41080  polvalN  41228  watvalN  41316  ldilset  41432  ltrnset  41441  dilsetN  41476  trnsetN  41479  trlset  41484  trlval  41485  cdleme16b  41602  cdleme31fv1  41714  cdlemg1idlemN  41895  tgrpset  42068  tendoset  42082  erngset  42123  erngplus  42126  erngmul  42129  erngset-rN  42131  erngplus-rN  42134  dvaset  42328  dvaplusg  42332  dvamulr  42335  dvavadd  42338  dvavsca  42340  diafval  42354  dvhset  42404  dvhmulr  42409  dvhvadd  42415  dvhvsca  42424  docafvalN  42445  djafvalN  42457  dibfval  42464  dicfval  42498  dihfval  42554  dihval  42555  dihvalc  42556  dihvalb  42560  dochfval  42673  djhfval  42720  lcdval  42912  mapdfval  42950  mapdn0  42992  hvmapfval  43082  hdmap1fval  43119  hdmapfval  43150  hgmapfval  43209  fmpocos  43554  sn-it0e0  43733  zaddcomlem  43793  pw2f1ocnv  44310  hbtlem7  44392  relexp0a  44977  ntrclscls00  45327  dvconstbi  45579  expgrowth  45580  addrfv  45711  subrfv  45712  mulvfv  45713  refsum2cnlem1  46328  limcperiod  46913  cncfiooiccre  47178  dvbdfbdioolem1  47211  itgioocnicc  47260  fourierdlem73  47462  fourierdlem82  47471  fourierdlem94  47483  fourierdlem103  47492  fourierdlem104  47493  fourierdlem113  47502  sqwvfoura  47511  etransclem46  47563  nnfoctbdjlem  47738  ovn0  47849  smflim  48060  afveu  48496  afv2eu  48581  fvmptrabdm  48636  imasetpreimafvbijlemfo  48760  lighneallem3  48965  ppivalnnprm  48983  mogoldbblem  49091  fpprel2  49112  sbgoldbwt  49148  nnsum4primeseven  49171  nnsum4primesevenALTV  49172  bgoldbtbnd  49180  grimco  49260  cycl3grtri  49318  lmod0rng  49599  lmodvsmdi  49822  lincdifsn  49867  lcoel0  49871  islindeps2  49926  blenn0  50016  nn0sumshdiglemA  50062  itcoval0mpt  50109  rrx2plordisom  50167  nelsubclem  50512  aacllem  51367