Theorem sylan9eq 2785

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 2750	. 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 2008  ax-9 2119  ax-ext 2702

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

This theorem is referenced by:  sylan9req  2786  sylan9eqr  2787  difeq12  4087  uneq12  4129  ineq12  4181  ssdifim  4239  ifeq12  4510  ifbi  4514  ifeq12da  4525  preq12  4702  prprc  4734  opeq12  4842  eqsnuniex  5319  opthwiener  5477  opthhausdorff0  5481  xpeq12  5666  sosn  5728  nfimad  6043  coi2  6239  funprg  6573  funtpg  6574  funcnvtp  6582  funcnvqp  6583  funimass1  6601  fimadmfoALT  6786  f1orescnv  6818  resdif  6824  fvmpt2  6982  fvmptnf  6993  fveqressseq  7054  oveq12  7399  cbvmpov  7487  ovmpog  7551  fvmpopr2d  7554  caofinvl  7688  eqopi  8007  el2mpocsbcl  8067  fmpoco  8077  mposn  8085  fsuppeqg  8158  supp0cosupp0  8190  imacosupp  8191  mpocurryd  8251  fvmpocurryd  8253  rdgsucmptf  8399  frsucmpt  8409  oevn0  8482  oa0r  8505  om1r  8510  oe1m  8512  omass  8547  oeoalem  8563  oeoa  8564  oeoe  8566  qseq12  8738  map0g  8860  xpcomco  9036  sbthlem4  9060  sbthlem5  9061  xpmapenlem  9114  phplem2  9175  unxpdomlem3  9206  funsnfsupp  9350  ordtypelem7  9484  ttrcltr  9676  cardennn  9943  dfac9  10097  alephsing  10236  axcc3  10398  ac6num  10439  konigthlem  10528  canthp1lem2  10613  ordpipq  10902  ltrnq  10939  addclprlem2  10977  mulclprlem  10979  prlem934  10993  prlem936  11007  mulcmpblnrlem  11030  addcnsr  11095  mulcnsr  11096  axcnre  11124  recex  11817  rpnnen1lem3  12945  rpnnen1lem5  12947  xaddpnf1  13193  xaddpnf2  13194  xaddmnf1  13195  xaddmnf2  13196  rexadd  13199  xnn0xaddcl  13202  xaddnemnf  13203  xaddnepnf  13204  xadddilem  13261  addmodlteq  13918  om2uzrani  13924  om2uzrdg  13928  seqf1olem2  14014  seqf1o  14015  modexp  14210  faclbnd4lem3  14267  hashunsng  14364  hashwrdn  14519  lsw1  14539  swrdfv  14620  swrdccat  14707  ccats1pfxeqbi  14714  revfv  14735  cshwsublen  14768  wrdlen2  14917  wrdl2exs2  14919  wwlktovf1  14930  relexp0  14996  relexpcnv  15008  shftcan1  15056  remul2  15103  immul2  15110  sumss  15697  geomulcvg  15849  fprodss  15921  binomfallfaclem2  16013  bpolylem  16021  ef0lem  16051  efieq1re  16174  rpnnen2lem1  16189  ruclem3  16208  dvdsnegb  16250  dvdscmul  16259  dvds2ln  16266  dvds2add  16267  dvds2sub  16268  gcdn0val  16475  rpmulgcd  16534  lcmn0val  16572  odzval  16769  pcval  16822  pcmpt  16870  prmreclem4  16897  1arithlem2  16902  vdwlem8  16966  ramcl2lem  16987  ramtcl  16988  ramtub  16990  ramcl2  16994  ramcl  17007  setsval  17144  prfcl  18171  curf1cl  18196  curfcl  18200  hofcl  18227  yonedalem4c  18245  psssdm  18548  grplactval  18981  mulgnn0gsum  19019  cntzval  19260  f1omvdco2  19385  pmtrfinv  19398  psgnunilem5  19431  odlem2  19476  gexlem2  19519  lsmvalx  19576  efgtval  19660  efgredlema  19677  vrgpval  19704  cyggex  19835  gsumcom2  19912  fincygsubgodd  20051  dvdsrtr  20284  rnghmval  20356  abvtrivd  20748  lmhmco  20957  reslmhm  20966  lvecinv  21030  zrhmulg  21426  znzrhval  21463  ocvval  21583  mplmon2  21975  subrgasclcl  21981  coe1fv  22098  coe1fzgsumdlem  22197  evl1gsumdlem  22250  mat1dimscm  22369  dmatid  22389  scmatdmat  22409  mavmul0g  22447  1marepvmarrepid  22469  mdetunilem2  22507  gsummatr01lem3  22551  gsummatr01  22553  smadiadetlem3  22562  m2cpminvid2lem  22648  chpdmatlem2  22733  isopn3  22960  cnpval  23130  ptbasfi  23475  dfac14  23512  cnmptkk  23577  xkofvcn  23578  cnmptk1p  23579  cnmptk2  23580  xkocnv  23708  flfval  23884  ptcmplem3  23948  ptcmpg  23951  tmdmulg  23986  prdsxmslem2  24424  subgnm2  24529  nmoval  24610  fsum2cn  24769  pcovalg  24919  isclmp  25004  cphnm  25100  tcphnmval  25136  ovolctb  25398  ioorcl  25485  uniioombllem2  25491  itg1addlem3  25606  itg1climres  25622  itg2uba  25651  itg2splitlem  25656  elcpn  25843  dvexp  25864  dvexp2  25865  rolle  25901  cmvth  25902  cmvthOLD  25903  mvth  25904  dvlip  25905  dvlipcn  25906  dvlip2  25907  dveq0  25912  dv11cn  25913  lhop1lem  25925  lhop2  25927  lhop  25928  dvcvx  25932  ftc2ditglem  25959  itgsubstlem  25962  ig1pval  26088  elply2  26108  coeid2  26151  coemul  26164  taylthlem2  26289  taylthlem2OLD  26290  ulmdvlem1  26316  mtest  26320  pserval2  26327  abelthlem1  26348  abelthlem3  26350  abelthlem8  26356  abelthlem9  26357  pige3ALT  26436  0cxp  26582  leibpi  26859  igamgam  26966  mule1  27065  bposlem5  27206  lgsval3  27233  lgsdinn0  27263  dchrvmasumlem1  27413  dchrisum0flblem1  27426  rpvmasum2  27430  padicval  27535  abssid  28150  abssnid  28152  axsegconlem1  28851  ax5seglem9  28871  axpasch  28875  axeuclidlem  28896  axcontlem2  28899  finsumvtxdg2ssteplem4  29483  usgr2wlkspthlem2  29695  crctcshlem4  29757  wwlknp  29780  wlkiswwlks2lem3  29808  wwlksnred  29829  wwlksnextproplem2  29847  umgrwwlks2on  29894  clwlkclwwlklem2a  29934  clwwisshclwwsn  29952  clwwlknlbonbgr1  29975  clwwlkn1loopb  29979  clwwlkf  29983  clwwlkext2edg  29992  wwlksext2clwwlk  29993  erclwwlknsym  30006  erclwwlkntr  30007  clwwlknon1  30033  clwwlknonex2  30045  eupth2lem3lem3  30166  eucrct2eupth  30181  fusgreghash2wspv  30271  2clwwlk2clwwlklem  30282  2clwwlk2clwwlk  30286  numclwwlk1lem2f1  30293  grpoidinvlem4  30443  grpoinvval  30459  grpodivval  30471  ipval  30639  sspgval  30665  sspsval  30667  sspnval  30673  nmooval  30699  ipasslem1  30767  ipasslem4  30770  hial0  31038  hial02  31039  ocsh  31219  pjhval  31333  hosval  31676  homval  31677  hodval  31678  hfsval  31679  hfmval  31680  braval  31880  kbval  31890  eigvalval  31896  0hmop  31919  adj0  31930  lnopeq0i  31943  nmopcoi  32031  pjclem4  32135  pj3si  32143  hstoh  32168  strlem3a  32188  hstrlem3a  32196  mdexchi  32271  atcv0eq  32315  atcv1  32316  fpwrelmap  32663  cycpmco2lem4  33093  cycpmco2lem5  33094  fxpgaval  33131  smatfval  33792  measxun2  34207  measdivcst  34221  measdivcstALTV  34222  ddeval1  34231  ddeval0  34232  ballotlemfp1  34490  signswmnd  34555  signstfvneq0  34570  signstfvc  34572  ftc2re  34596  itgexpif  34604  bnj1128  34987  subfacp1lem3  35176  subfacp1lem5  35178  cvmlift2lem3  35299  msubco  35525  altopthsn  35956  ditgeq12d  36217  fnetr  36346  fnejoin2  36364  bj-evalid  37071  finxpreclem3  37388  finxpreclem5  37390  finxpreclem6  37391  curf  37599  curunc  37603  matunitlindf  37619  poimirlem4  37625  poimirlem25  37646  mblfinlem2  37659  mblfinlem3  37660  mbfresfi  37667  itg2addnclem  37672  itg2addnc  37675  ftc1anclem5  37698  isbnd3  37785  bndss  37787  grposnOLD  37883  ghomco  37892  xrneq12  38376  lkrval  39088  pmapval  39758  polvalN  39906  watvalN  39994  ldilset  40110  ltrnset  40119  dilsetN  40154  trnsetN  40157  trlset  40162  trlval  40163  cdleme16b  40280  cdleme31fv1  40392  cdlemg1idlemN  40573  tgrpset  40746  tendoset  40760  erngset  40801  erngplus  40804  erngmul  40807  erngset-rN  40809  erngplus-rN  40812  dvaset  41006  dvaplusg  41010  dvamulr  41013  dvavadd  41016  dvavsca  41018  diafval  41032  dvhset  41082  dvhmulr  41087  dvhvadd  41093  dvhvsca  41102  docafvalN  41123  djafvalN  41135  dibfval  41142  dicfval  41176  dihfval  41232  dihval  41233  dihvalc  41234  dihvalb  41238  dochfval  41351  djhfval  41398  lcdval  41590  mapdfval  41628  mapdn0  41670  hvmapfval  41760  hdmap1fval  41797  hdmapfval  41828  hgmapfval  41887  fmpocos  42229  sn-it0e0  42411  zaddcomlem  42458  pw2f1ocnv  43033  hbtlem7  43121  relexp0a  43712  ntrclscls00  44062  dvconstbi  44330  expgrowth  44331  addrfv  44465  subrfv  44466  mulvfv  44467  refsum2cnlem1  45038  limcperiod  45633  cncfiooiccre  45900  dvbdfbdioolem1  45933  itgioocnicc  45982  fourierdlem73  46184  fourierdlem82  46193  fourierdlem94  46205  fourierdlem103  46214  fourierdlem104  46215  fourierdlem113  46224  sqwvfoura  46233  etransclem46  46285  nnfoctbdjlem  46460  ovn0  46571  smflim  46782  afveu  47158  afv2eu  47243  fvmptrabdm  47298  imasetpreimafvbijlemfo  47410  lighneallem3  47612  mogoldbblem  47725  fpprel2  47746  sbgoldbwt  47782  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  bgoldbtbnd  47814  grimco  47893  cycl3grtri  47950  lmod0rng  48221  lmodvsmdi  48371  lincdifsn  48417  lcoel0  48421  islindeps2  48476  blenn0  48566  nn0sumshdiglemA  48612  itcoval0mpt  48659  rrx2plordisom  48716  nelsubclem  49060  aacllem  49794