Theorem sylan9eq 2784

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 2749	. 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 2701

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

This theorem is referenced by:  sylan9req  2785  sylan9eqr  2786  difeq12  4072  uneq12  4114  ineq12  4166  ssdifim  4224  ifeq12  4495  ifbi  4499  ifeq12da  4510  preq12  4687  prprc  4719  opeq12  4826  eqsnuniex  5300  opthwiener  5457  opthhausdorff0  5461  xpeq12  5644  sosn  5706  nfimad  6020  coi2  6212  funprg  6536  funtpg  6537  funcnvtp  6545  funcnvqp  6546  funimass1  6564  fimadmfoALT  6747  f1orescnv  6779  resdif  6785  fvmpt2  6941  fvmptnf  6952  fveqressseq  7013  oveq12  7358  cbvmpov  7444  ovmpog  7508  fvmpopr2d  7511  caofinvl  7645  eqopi  7960  el2mpocsbcl  8018  fmpoco  8028  mposn  8036  fsuppeqg  8109  supp0cosupp0  8141  imacosupp  8142  mpocurryd  8202  fvmpocurryd  8204  rdgsucmptf  8350  frsucmpt  8360  oevn0  8433  oa0r  8456  om1r  8461  oe1m  8463  omass  8498  oeoalem  8514  oeoa  8515  oeoe  8517  qseq12  8689  map0g  8811  xpcomco  8984  sbthlem4  9007  sbthlem5  9008  xpmapenlem  9061  phplem2  9119  unxpdomlem3  9147  funsnfsupp  9282  ordtypelem7  9416  ttrcltr  9612  cardennn  9879  dfac9  10031  alephsing  10170  axcc3  10332  ac6num  10373  konigthlem  10462  canthp1lem2  10547  ordpipq  10836  ltrnq  10873  addclprlem2  10911  mulclprlem  10913  prlem934  10927  prlem936  10941  mulcmpblnrlem  10964  addcnsr  11029  mulcnsr  11030  axcnre  11058  recex  11752  rpnnen1lem3  12880  rpnnen1lem5  12882  xaddpnf1  13128  xaddpnf2  13129  xaddmnf1  13130  xaddmnf2  13131  rexadd  13134  xnn0xaddcl  13137  xaddnemnf  13138  xaddnepnf  13139  xadddilem  13196  addmodlteq  13853  om2uzrani  13859  om2uzrdg  13863  seqf1olem2  13949  seqf1o  13950  modexp  14145  faclbnd4lem3  14202  hashunsng  14299  hashwrdn  14454  lsw1  14474  swrdfv  14555  swrdccat  14641  ccats1pfxeqbi  14648  revfv  14669  cshwsublen  14702  wrdlen2  14851  wrdl2exs2  14853  wwlktovf1  14864  relexp0  14930  relexpcnv  14942  shftcan1  14990  remul2  15037  immul2  15044  sumss  15631  geomulcvg  15783  fprodss  15855  binomfallfaclem2  15947  bpolylem  15955  ef0lem  15985  efieq1re  16108  rpnnen2lem1  16123  ruclem3  16142  dvdsnegb  16184  dvdscmul  16193  dvds2ln  16200  dvds2add  16201  dvds2sub  16202  gcdn0val  16409  rpmulgcd  16468  lcmn0val  16506  odzval  16703  pcval  16756  pcmpt  16804  prmreclem4  16831  1arithlem2  16836  vdwlem8  16900  ramcl2lem  16921  ramtcl  16922  ramtub  16924  ramcl2  16928  ramcl  16941  setsval  17078  prfcl  18109  curf1cl  18134  curfcl  18138  hofcl  18165  yonedalem4c  18183  psssdm  18488  grplactval  18921  mulgnn0gsum  18959  cntzval  19200  f1omvdco2  19327  pmtrfinv  19340  psgnunilem5  19373  odlem2  19418  gexlem2  19461  lsmvalx  19518  efgtval  19602  efgredlema  19619  vrgpval  19646  cyggex  19777  gsumcom2  19854  fincygsubgodd  19993  dvdsrtr  20253  rnghmval  20325  abvtrivd  20717  lmhmco  20947  reslmhm  20956  lvecinv  21020  zrhmulg  21416  znzrhval  21453  ocvval  21574  mplmon2  21966  subrgasclcl  21972  coe1fv  22089  coe1fzgsumdlem  22188  evl1gsumdlem  22241  mat1dimscm  22360  dmatid  22380  scmatdmat  22400  mavmul0g  22438  1marepvmarrepid  22460  mdetunilem2  22498  gsummatr01lem3  22542  gsummatr01  22544  smadiadetlem3  22553  m2cpminvid2lem  22639  chpdmatlem2  22724  isopn3  22951  cnpval  23121  ptbasfi  23466  dfac14  23503  cnmptkk  23568  xkofvcn  23569  cnmptk1p  23570  cnmptk2  23571  xkocnv  23699  flfval  23875  ptcmplem3  23939  ptcmpg  23942  tmdmulg  23977  prdsxmslem2  24415  subgnm2  24520  nmoval  24601  fsum2cn  24760  pcovalg  24910  isclmp  24995  cphnm  25091  tcphnmval  25127  ovolctb  25389  ioorcl  25476  uniioombllem2  25482  itg1addlem3  25597  itg1climres  25613  itg2uba  25642  itg2splitlem  25647  elcpn  25834  dvexp  25855  dvexp2  25856  rolle  25892  cmvth  25893  cmvthOLD  25894  mvth  25895  dvlip  25896  dvlipcn  25897  dvlip2  25898  dveq0  25903  dv11cn  25904  lhop1lem  25916  lhop2  25918  lhop  25919  dvcvx  25923  ftc2ditglem  25950  itgsubstlem  25953  ig1pval  26079  elply2  26099  coeid2  26142  coemul  26155  taylthlem2  26280  taylthlem2OLD  26281  ulmdvlem1  26307  mtest  26311  pserval2  26318  abelthlem1  26339  abelthlem3  26341  abelthlem8  26347  abelthlem9  26348  pige3ALT  26427  0cxp  26573  leibpi  26850  igamgam  26957  mule1  27056  bposlem5  27197  lgsval3  27224  lgsdinn0  27254  dchrvmasumlem1  27404  dchrisum0flblem1  27417  rpvmasum2  27421  padicval  27526  abssid  28148  abssnid  28150  axsegconlem1  28862  ax5seglem9  28882  axpasch  28886  axeuclidlem  28907  axcontlem2  28910  finsumvtxdg2ssteplem4  29494  usgr2wlkspthlem2  29703  crctcshlem4  29765  wwlknp  29788  wlkiswwlks2lem3  29816  wwlksnred  29837  wwlksnextproplem2  29855  umgrwwlks2on  29902  clwlkclwwlklem2a  29942  clwwisshclwwsn  29960  clwwlknlbonbgr1  29983  clwwlkn1loopb  29987  clwwlkf  29991  clwwlkext2edg  30000  wwlksext2clwwlk  30001  erclwwlknsym  30014  erclwwlkntr  30015  clwwlknon1  30041  clwwlknonex2  30053  eupth2lem3lem3  30174  eucrct2eupth  30189  fusgreghash2wspv  30279  2clwwlk2clwwlklem  30290  2clwwlk2clwwlk  30294  numclwwlk1lem2f1  30301  grpoidinvlem4  30451  grpoinvval  30467  grpodivval  30479  ipval  30647  sspgval  30673  sspsval  30675  sspnval  30681  nmooval  30707  ipasslem1  30775  ipasslem4  30778  hial0  31046  hial02  31047  ocsh  31227  pjhval  31341  hosval  31684  homval  31685  hodval  31686  hfsval  31687  hfmval  31688  braval  31888  kbval  31898  eigvalval  31904  0hmop  31927  adj0  31938  lnopeq0i  31951  nmopcoi  32039  pjclem4  32143  pj3si  32151  hstoh  32176  strlem3a  32196  hstrlem3a  32204  mdexchi  32279  atcv0eq  32323  atcv1  32324  fpwrelmap  32676  cycpmco2lem4  33071  cycpmco2lem5  33072  fxpgaval  33109  smatfval  33762  measxun2  34177  measdivcst  34191  measdivcstALTV  34192  ddeval1  34201  ddeval0  34202  ballotlemfp1  34460  signswmnd  34525  signstfvneq0  34540  signstfvc  34542  ftc2re  34566  itgexpif  34574  bnj1128  34957  subfacp1lem3  35155  subfacp1lem5  35157  cvmlift2lem3  35278  msubco  35504  altopthsn  35935  ditgeq12d  36196  fnetr  36325  fnejoin2  36343  bj-evalid  37050  finxpreclem3  37367  finxpreclem5  37369  finxpreclem6  37370  curf  37578  curunc  37582  matunitlindf  37598  poimirlem4  37604  poimirlem25  37625  mblfinlem2  37638  mblfinlem3  37639  mbfresfi  37646  itg2addnclem  37651  itg2addnc  37654  ftc1anclem5  37677  isbnd3  37764  bndss  37766  grposnOLD  37862  ghomco  37871  xrneq12  38355  lkrval  39067  pmapval  39736  polvalN  39884  watvalN  39972  ldilset  40088  ltrnset  40097  dilsetN  40132  trnsetN  40135  trlset  40140  trlval  40141  cdleme16b  40258  cdleme31fv1  40370  cdlemg1idlemN  40551  tgrpset  40724  tendoset  40738  erngset  40779  erngplus  40782  erngmul  40785  erngset-rN  40787  erngplus-rN  40790  dvaset  40984  dvaplusg  40988  dvamulr  40991  dvavadd  40994  dvavsca  40996  diafval  41010  dvhset  41060  dvhmulr  41065  dvhvadd  41071  dvhvsca  41080  docafvalN  41101  djafvalN  41113  dibfval  41120  dicfval  41154  dihfval  41210  dihval  41211  dihvalc  41212  dihvalb  41216  dochfval  41329  djhfval  41376  lcdval  41568  mapdfval  41606  mapdn0  41648  hvmapfval  41738  hdmap1fval  41775  hdmapfval  41806  hgmapfval  41865  fmpocos  42207  sn-it0e0  42389  zaddcomlem  42436  pw2f1ocnv  43010  hbtlem7  43098  relexp0a  43689  ntrclscls00  44039  dvconstbi  44307  expgrowth  44308  addrfv  44442  subrfv  44443  mulvfv  44444  refsum2cnlem1  45015  limcperiod  45609  cncfiooiccre  45876  dvbdfbdioolem1  45909  itgioocnicc  45958  fourierdlem73  46160  fourierdlem82  46169  fourierdlem94  46181  fourierdlem103  46190  fourierdlem104  46191  fourierdlem113  46200  sqwvfoura  46209  etransclem46  46261  nnfoctbdjlem  46436  ovn0  46547  smflim  46758  afveu  47137  afv2eu  47222  fvmptrabdm  47277  imasetpreimafvbijlemfo  47389  lighneallem3  47591  mogoldbblem  47704  fpprel2  47725  sbgoldbwt  47761  nnsum4primeseven  47784  nnsum4primesevenALTV  47785  bgoldbtbnd  47793  grimco  47873  cycl3grtri  47931  lmod0rng  48213  lmodvsmdi  48363  lincdifsn  48409  lcoel0  48413  islindeps2  48468  blenn0  48558  nn0sumshdiglemA  48604  itcoval0mpt  48651  rrx2plordisom  48708  nelsubclem  49052  aacllem  49786