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  4084  uneq12  4126  ineq12  4178  ssdifim  4236  ifeq12  4507  ifbi  4511  ifeq12da  4522  preq12  4699  prprc  4731  opeq12  4839  eqsnuniex  5316  opthwiener  5474  opthhausdorff0  5478  xpeq12  5663  sosn  5725  nfimad  6040  coi2  6236  funprg  6570  funtpg  6571  funcnvtp  6579  funcnvqp  6580  funimass1  6598  fimadmfoALT  6783  f1orescnv  6815  resdif  6821  fvmpt2  6979  fvmptnf  6990  fveqressseq  7051  oveq12  7396  cbvmpov  7484  ovmpog  7548  fvmpopr2d  7551  caofinvl  7685  eqopi  8004  el2mpocsbcl  8064  fmpoco  8074  mposn  8082  fsuppeqg  8155  supp0cosupp0  8187  imacosupp  8188  mpocurryd  8248  fvmpocurryd  8250  rdgsucmptf  8396  frsucmpt  8406  oevn0  8479  oa0r  8502  om1r  8507  oe1m  8509  omass  8544  oeoalem  8560  oeoa  8561  oeoe  8563  qseq12  8735  map0g  8857  xpcomco  9031  sbthlem4  9054  sbthlem5  9055  xpmapenlem  9108  phplem2  9169  unxpdomlem3  9199  funsnfsupp  9343  ordtypelem7  9477  ttrcltr  9669  cardennn  9936  dfac9  10090  alephsing  10229  axcc3  10391  ac6num  10432  konigthlem  10521  canthp1lem2  10606  ordpipq  10895  ltrnq  10932  addclprlem2  10970  mulclprlem  10972  prlem934  10986  prlem936  11000  mulcmpblnrlem  11023  addcnsr  11088  mulcnsr  11089  axcnre  11117  recex  11810  rpnnen1lem3  12938  rpnnen1lem5  12940  xaddpnf1  13186  xaddpnf2  13187  xaddmnf1  13188  xaddmnf2  13189  rexadd  13192  xnn0xaddcl  13195  xaddnemnf  13196  xaddnepnf  13197  xadddilem  13254  addmodlteq  13911  om2uzrani  13917  om2uzrdg  13921  seqf1olem2  14007  seqf1o  14008  modexp  14203  faclbnd4lem3  14260  hashunsng  14357  hashwrdn  14512  lsw1  14532  swrdfv  14613  swrdccat  14700  ccats1pfxeqbi  14707  revfv  14728  cshwsublen  14761  wrdlen2  14910  wrdl2exs2  14912  wwlktovf1  14923  relexp0  14989  relexpcnv  15001  shftcan1  15049  remul2  15096  immul2  15103  sumss  15690  geomulcvg  15842  fprodss  15914  binomfallfaclem2  16006  bpolylem  16014  ef0lem  16044  efieq1re  16167  rpnnen2lem1  16182  ruclem3  16201  dvdsnegb  16243  dvdscmul  16252  dvds2ln  16259  dvds2add  16260  dvds2sub  16261  gcdn0val  16468  rpmulgcd  16527  lcmn0val  16565  odzval  16762  pcval  16815  pcmpt  16863  prmreclem4  16890  1arithlem2  16895  vdwlem8  16959  ramcl2lem  16980  ramtcl  16981  ramtub  16983  ramcl2  16987  ramcl  17000  setsval  17137  prfcl  18164  curf1cl  18189  curfcl  18193  hofcl  18220  yonedalem4c  18238  psssdm  18541  grplactval  18974  mulgnn0gsum  19012  cntzval  19253  f1omvdco2  19378  pmtrfinv  19391  psgnunilem5  19424  odlem2  19469  gexlem2  19512  lsmvalx  19569  efgtval  19653  efgredlema  19670  vrgpval  19697  cyggex  19828  gsumcom2  19905  fincygsubgodd  20044  dvdsrtr  20277  rnghmval  20349  abvtrivd  20741  lmhmco  20950  reslmhm  20959  lvecinv  21023  zrhmulg  21419  znzrhval  21456  ocvval  21576  mplmon2  21968  subrgasclcl  21974  coe1fv  22091  coe1fzgsumdlem  22190  evl1gsumdlem  22243  mat1dimscm  22362  dmatid  22382  scmatdmat  22402  mavmul0g  22440  1marepvmarrepid  22462  mdetunilem2  22500  gsummatr01lem3  22544  gsummatr01  22546  smadiadetlem3  22555  m2cpminvid2lem  22641  chpdmatlem2  22726  isopn3  22953  cnpval  23123  ptbasfi  23468  dfac14  23505  cnmptkk  23570  xkofvcn  23571  cnmptk1p  23572  cnmptk2  23573  xkocnv  23701  flfval  23877  ptcmplem3  23941  ptcmpg  23944  tmdmulg  23979  prdsxmslem2  24417  subgnm2  24522  nmoval  24603  fsum2cn  24762  pcovalg  24912  isclmp  24997  cphnm  25093  tcphnmval  25129  ovolctb  25391  ioorcl  25478  uniioombllem2  25484  itg1addlem3  25599  itg1climres  25615  itg2uba  25644  itg2splitlem  25649  elcpn  25836  dvexp  25857  dvexp2  25858  rolle  25894  cmvth  25895  cmvthOLD  25896  mvth  25897  dvlip  25898  dvlipcn  25899  dvlip2  25900  dveq0  25905  dv11cn  25906  lhop1lem  25918  lhop2  25920  lhop  25921  dvcvx  25925  ftc2ditglem  25952  itgsubstlem  25955  ig1pval  26081  elply2  26101  coeid2  26144  coemul  26157  taylthlem2  26282  taylthlem2OLD  26283  ulmdvlem1  26309  mtest  26313  pserval2  26320  abelthlem1  26341  abelthlem3  26343  abelthlem8  26349  abelthlem9  26350  pige3ALT  26429  0cxp  26575  leibpi  26852  igamgam  26959  mule1  27058  bposlem5  27199  lgsval3  27226  lgsdinn0  27256  dchrvmasumlem1  27406  dchrisum0flblem1  27419  rpvmasum2  27423  padicval  27528  abssid  28143  abssnid  28145  axsegconlem1  28844  ax5seglem9  28864  axpasch  28868  axeuclidlem  28889  axcontlem2  28892  finsumvtxdg2ssteplem4  29476  usgr2wlkspthlem2  29688  crctcshlem4  29750  wwlknp  29773  wlkiswwlks2lem3  29801  wwlksnred  29822  wwlksnextproplem2  29840  umgrwwlks2on  29887  clwlkclwwlklem2a  29927  clwwisshclwwsn  29945  clwwlknlbonbgr1  29968  clwwlkn1loopb  29972  clwwlkf  29976  clwwlkext2edg  29985  wwlksext2clwwlk  29986  erclwwlknsym  29999  erclwwlkntr  30000  clwwlknon1  30026  clwwlknonex2  30038  eupth2lem3lem3  30159  eucrct2eupth  30174  fusgreghash2wspv  30264  2clwwlk2clwwlklem  30275  2clwwlk2clwwlk  30279  numclwwlk1lem2f1  30286  grpoidinvlem4  30436  grpoinvval  30452  grpodivval  30464  ipval  30632  sspgval  30658  sspsval  30660  sspnval  30666  nmooval  30692  ipasslem1  30760  ipasslem4  30763  hial0  31031  hial02  31032  ocsh  31212  pjhval  31326  hosval  31669  homval  31670  hodval  31671  hfsval  31672  hfmval  31673  braval  31873  kbval  31883  eigvalval  31889  0hmop  31912  adj0  31923  lnopeq0i  31936  nmopcoi  32024  pjclem4  32128  pj3si  32136  hstoh  32161  strlem3a  32181  hstrlem3a  32189  mdexchi  32264  atcv0eq  32308  atcv1  32309  fpwrelmap  32656  cycpmco2lem4  33086  cycpmco2lem5  33087  fxpgaval  33124  smatfval  33785  measxun2  34200  measdivcst  34214  measdivcstALTV  34215  ddeval1  34224  ddeval0  34225  ballotlemfp1  34483  signswmnd  34548  signstfvneq0  34563  signstfvc  34565  ftc2re  34589  itgexpif  34597  bnj1128  34980  subfacp1lem3  35169  subfacp1lem5  35171  cvmlift2lem3  35292  msubco  35518  altopthsn  35949  ditgeq12d  36210  fnetr  36339  fnejoin2  36357  bj-evalid  37064  finxpreclem3  37381  finxpreclem5  37383  finxpreclem6  37384  curf  37592  curunc  37596  matunitlindf  37612  poimirlem4  37618  poimirlem25  37639  mblfinlem2  37652  mblfinlem3  37653  mbfresfi  37660  itg2addnclem  37665  itg2addnc  37668  ftc1anclem5  37691  isbnd3  37778  bndss  37780  grposnOLD  37876  ghomco  37885  xrneq12  38369  lkrval  39081  pmapval  39751  polvalN  39899  watvalN  39987  ldilset  40103  ltrnset  40112  dilsetN  40147  trnsetN  40150  trlset  40155  trlval  40156  cdleme16b  40273  cdleme31fv1  40385  cdlemg1idlemN  40566  tgrpset  40739  tendoset  40753  erngset  40794  erngplus  40797  erngmul  40800  erngset-rN  40802  erngplus-rN  40805  dvaset  40999  dvaplusg  41003  dvamulr  41006  dvavadd  41009  dvavsca  41011  diafval  41025  dvhset  41075  dvhmulr  41080  dvhvadd  41086  dvhvsca  41095  docafvalN  41116  djafvalN  41128  dibfval  41135  dicfval  41169  dihfval  41225  dihval  41226  dihvalc  41227  dihvalb  41231  dochfval  41344  djhfval  41391  lcdval  41583  mapdfval  41621  mapdn0  41663  hvmapfval  41753  hdmap1fval  41790  hdmapfval  41821  hgmapfval  41880  fmpocos  42222  sn-it0e0  42404  zaddcomlem  42451  pw2f1ocnv  43026  hbtlem7  43114  relexp0a  43705  ntrclscls00  44055  dvconstbi  44323  expgrowth  44324  addrfv  44458  subrfv  44459  mulvfv  44460  refsum2cnlem1  45031  limcperiod  45626  cncfiooiccre  45893  dvbdfbdioolem1  45926  itgioocnicc  45975  fourierdlem73  46177  fourierdlem82  46186  fourierdlem94  46198  fourierdlem103  46207  fourierdlem104  46208  fourierdlem113  46217  sqwvfoura  46226  etransclem46  46278  nnfoctbdjlem  46453  ovn0  46564  smflim  46775  afveu  47154  afv2eu  47239  fvmptrabdm  47294  imasetpreimafvbijlemfo  47406  lighneallem3  47608  mogoldbblem  47721  fpprel2  47742  sbgoldbwt  47778  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  bgoldbtbnd  47810  grimco  47889  cycl3grtri  47946  lmod0rng  48217  lmodvsmdi  48367  lincdifsn  48413  lcoel0  48417  islindeps2  48472  blenn0  48562  nn0sumshdiglemA  48608  itcoval0mpt  48655  rrx2plordisom  48712  nelsubclem  49056  aacllem  49790