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 607	1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  sylan9req  2819  sylan9eqr  2820  difeq12  4076  uneq12  4117  ineq12  4168  ssdifim  4226  ifeq12  4506  ifbi  4510  ifeq12da  4521  preq12  4701  prprc  4733  opeq12  4840  eqsnuniex  5332  opthwiener  5497  opthhausdorff0  5501  xpeq12  5686  sosn  5748  nfimad  6071  coi2  6265  funprg  6590  funtpg  6591  funcnvtp  6599  funcnvqp  6600  funimass1  6618  fimadmfoALT  6803  f1orescnv  6836  resdif  6842  fvmpt2  7001  fvmptnf  7012  fveqressseq  7074  oveq12  7419  cbvmpov  7505  ovmpog  7569  fvmpopr2d  7572  caofinvl  7706  eqopi  8018  el2mpocsbcl  8076  fmpoco  8086  mposn  8094  fsuppeqg  8168  supp0cosupp0  8200  imacosupp  8201  mpocurryd  8261  fvmpocurryd  8263  rdgsucmptf  8411  frsucmpt  8421  oevn0  8496  oa0r  8519  om1r  8524  oe1m  8526  omass  8561  oeoalem  8578  oeoa  8579  oeoe  8581  qseq12  8755  map0g  8878  xpcomco  9051  sbthlem4  9074  sbthlem5  9075  xpmapenlem  9128  phplem2  9185  unxpdomlem3  9214  funsnfsupp  9348  ordtypelem7  9482  ttrcltr  9681  cardennn  9965  dfac9  10116  alephsing  10255  axcc3  10417  ac6num  10458  konigthlem  10548  canthp1lem2  10633  ordpipq  10922  ltrnq  10959  addclprlem2  10997  mulclprlem  10999  prlem934  11013  prlem936  11027  mulcmpblnrlem  11050  addcnsr  11115  mulcnsr  11116  axcnre  11144  recex  11841  rpnnen1lem3  12998  rpnnen1lem5  13000  xaddpnf1  13247  xaddpnf2  13248  xaddmnf1  13249  xaddmnf2  13250  rexadd  13253  xnn0xaddcl  13256  xaddnemnf  13257  xaddnepnf  13258  xadddilem  13315  addmodlteq  13978  om2uzrani  13984  om2uzrdg  13988  seqf1olem2  14074  seqf1o  14075  modexp  14270  faclbnd4lem3  14327  hashunsng  14424  hashwrdn  14580  lsw1  14600  swrdfv  14682  swrdccat  14768  ccats1pfxeqbi  14775  revfv  14796  cshwsublen  14829  wrdlen2  14977  wrdl2exs2  14979  wwlktovf1  14990  relexp0  15056  relexpcnv  15068  shftcan1  15116  remul2  15177  immul2  15184  sumss  15771  geomulcvg  15926  fprodss  15998  binomfallfaclem2  16089  bpolylem  16097  ef0lem  16127  efieq1re  16250  rpnnen2lem1  16265  ruclem3  16284  dvdsnegb  16326  dvdscmul  16335  dvds2ln  16342  dvds2add  16343  dvds2sub  16344  gcdn0val  16551  rpmulgcd  16610  lcmn0val  16648  odzval  16846  pcval  16899  pcmpt  16947  prmreclem4  16974  1arithlem2  16979  vdwlem8  17043  ramcl2lem  17064  ramtcl  17065  ramtub  17067  ramcl2  17071  ramcl  17084  setsval  17222  prfcl  18254  curf1cl  18279  curfcl  18283  hofcl  18310  yonedalem4c  18328  psssdm  18633  chneq12  18665  grplactval  19103  mulgnn0gsum  19141  cntzval  19386  f1omvdco2  19513  pmtrfinv  19526  psgnunilem5  19559  odlem2  19604  gexlem2  19647  lsmvalx  19704  efgtval  19788  efgredlema  19805  vrgpval  19832  cyggex  19963  gsumcom2  20040  fincygsubgodd  20179  dvdsrtr  20446  rnghmval  20518  abvtrivd  20935  lmhmco  21164  reslmhm  21173  lvecinv  21237  zrhmulg  21659  znzrhval  21696  ocvval  21817  mplmon2  22212  subrgasclcl  22218  coe1fv  22366  coe1fzgsumdlem  22463  evl1gsumdlem  22516  mat1dimscm  22632  dmatid  22652  scmatdmat  22672  mavmul0g  22710  1marepvmarrepid  22732  mdetunilem2  22770  gsummatr01lem3  22814  gsummatr01  22816  smadiadetlem3  22825  m2cpminvid2lem  22911  chpdmatlem2  22996  isopn3  23223  cnpval  23393  ptbasfi  23738  dfac14  23775  cnmptkk  23840  xkofvcn  23841  cnmptk1p  23842  cnmptk2  23843  xkocnv  23971  flfval  24147  ptcmplem3  24211  ptcmpg  24214  tmdmulg  24249  prdsxmslem2  24686  subgnm2  24791  nmoval  24872  fsum2cn  25030  pcovalg  25171  isclmp  25256  cphnm  25352  tcphnmval  25388  ovolctb  25649  ioorcl  25736  uniioombllem2  25742  itg1addlem3  25857  itg1climres  25873  itg2uba  25902  itg2splitlem  25907  elcpn  26093  dvexp  26112  dvexp2  26113  rolle  26149  cmvth  26150  mvth  26151  dvlip  26152  dvlipcn  26153  dvlip2  26154  dveq0  26159  dv11cn  26160  lhop1lem  26172  lhop2  26174  lhop  26175  dvcvx  26179  ftc2ditglem  26204  itgsubstlem  26207  ig1pval  26333  elply2  26353  coeid2  26396  coemul  26409  taylthlem2  26537  ulmdvlem1  26563  mtest  26567  pserval2  26574  abelthlem1  26594  abelthlem3  26596  abelthlem8  26602  abelthlem9  26603  pige3ALT  26685  0cxp  26831  leibpi  27107  igamgam  27213  mule1  27312  bposlem5  27452  lgsval3  27479  lgsdinn0  27509  dchrvmasumlem1  27659  dchrisum0flblem1  27672  rpvmasum2  27676  padicval  27781  abssid  28434  abssnid  28436  axsegconlem1  29267  ax5seglem9  29287  axpasch  29291  axeuclidlem  29312  axcontlem2  29315  finsumvtxdg2ssteplem4  29898  usgr2wlkspthlem2  30107  crctcshlem4  30169  wwlknp  30192  wlkiswwlks2lem3  30220  wwlksnred  30241  wwlksnextproplem2  30259  usgrwwlks2on  30307  umgrwwlks2on  30308  clwlkclwwlklem2a  30349  clwwisshclwwsn  30367  clwwlknlbonbgr1  30390  clwwlkn1loopb  30394  clwwlkf  30398  clwwlkext2edg  30407  wwlksext2clwwlk  30408  erclwwlknsym  30421  erclwwlkntr  30422  clwwlknon1  30448  clwwlknonex2  30460  eupth2lem3lem3  30581  eucrct2eupth  30596  fusgreghash2wspv  30686  2clwwlk2clwwlklem  30697  2clwwlk2clwwlk  30701  numclwwlk1lem2f1  30708  grpoidinvlem4  30859  grpoinvval  30875  grpodivval  30887  ipval  31055  sspgval  31081  sspsval  31083  sspnval  31089  nmooval  31115  ipasslem1  31183  ipasslem4  31186  hial0  31454  hial02  31455  ocsh  31635  pjhval  31749  hosval  32092  homval  32093  hodval  32094  hfsval  32095  hfmval  32096  braval  32296  kbval  32306  eigvalval  32312  0hmop  32335  adj0  32346  lnopeq0i  32359  nmopcoi  32447  pjclem4  32551  pj3si  32559  hstoh  32584  strlem3a  32604  hstrlem3a  32612  mdexchi  32687  atcv0eq  32731  atcv1  32732  fpwrelmap  33078  cycpmco2lem4  33449  cycpmco2lem5  33450  fxpgaval  33487  smatfval  34185  measxun2  34600  measdivcst  34614  measdivcstALTV  34615  ddeval1  34624  ddeval0  34625  ballotlemfp1  34882  signswmnd  34944  signstfvneq0  34959  signstfvc  34961  ftc2re  34985  itgexpif  34993  bnj1128  35378  subfacp1lem3  35674  subfacp1lem5  35676  cvmlift2lem3  35797  msubco  36023  altopthsn  36453  ditgeq12d  36734  fnetr  36862  fnejoin2  36880  ttcsntrsucg  37033  bj-evalid  37718  finxpreclem3  38039  finxpreclem5  38041  finxpreclem6  38042  curf  38249  curunc  38253  matunitlindf  38269  poimirlem4  38275  poimirlem25  38296  mblfinlem2  38309  mblfinlem3  38310  mbfresfi  38317  itg2addnclem  38322  itg2addnc  38325  ftc1anclem5  38348  isbnd3  38435  bndss  38437  grposnOLD  38533  ghomco  38542  xrneq12  39051  lkrval  39862  pmapval  40531  polvalN  40679  watvalN  40767  ldilset  40883  ltrnset  40892  dilsetN  40927  trnsetN  40930  trlset  40935  trlval  40936  cdleme16b  41053  cdleme31fv1  41165  cdlemg1idlemN  41346  tgrpset  41519  tendoset  41533  erngset  41574  erngplus  41577  erngmul  41580  erngset-rN  41582  erngplus-rN  41585  dvaset  41779  dvaplusg  41783  dvamulr  41786  dvavadd  41789  dvavsca  41791  diafval  41805  dvhset  41855  dvhmulr  41860  dvhvadd  41866  dvhvsca  41875  docafvalN  41896  djafvalN  41908  dibfval  41915  dicfval  41949  dihfval  42005  dihval  42006  dihvalc  42007  dihvalb  42011  dochfval  42124  djhfval  42171  lcdval  42363  mapdfval  42401  mapdn0  42443  hvmapfval  42533  hdmap1fval  42570  hdmapfval  42601  hgmapfval  42660  fmpocos  43004  sn-it0e0  43177  zaddcomlem  43237  pw2f1ocnv  43764  hbtlem7  43852  relexp0a  44442  ntrclscls00  44792  dvconstbi  45044  expgrowth  45045  addrfv  45177  subrfv  45178  mulvfv  45179  refsum2cnlem1  45757  limcperiod  46344  cncfiooiccre  46609  dvbdfbdioolem1  46642  itgioocnicc  46691  fourierdlem73  46893  fourierdlem82  46902  fourierdlem94  46914  fourierdlem103  46923  fourierdlem104  46924  fourierdlem113  46933  sqwvfoura  46942  etransclem46  46994  nnfoctbdjlem  47169  ovn0  47280  smflim  47491  afveu  47890  afv2eu  47975  fvmptrabdm  48030  imasetpreimafvbijlemfo  48154  lighneallem3  48359  ppivalnnprm  48377  mogoldbblem  48485  fpprel2  48506  sbgoldbwt  48542  nnsum4primeseven  48565  nnsum4primesevenALTV  48566  bgoldbtbnd  48574  grimco  48654  cycl3grtri  48712  lmod0rng  48994  lmodvsmdi  49159  lincdifsn  49204  lcoel0  49208  islindeps2  49263  blenn0  49353  nn0sumshdiglemA  49399  itcoval0mpt  49446  rrx2plordisom  49503  nelsubclem  49845  aacllem  50621