Theorem sylan9eq 2816

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 2781	. 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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

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

This theorem is used by:  sylan9req  2817  sylan9eqr  2818  difeq12  4069  uneq12  4110  ineq12  4161  ssdifim  4219  ifeq12  4501  ifbi  4505  ifeq12da  4516  preq12  4696  prprc  4728  opeq12  4835  eqsnuniex  5323  opthwiener  5487  opthhausdorff0  5491  xpeq12  5676  sosn  5738  nfimad  6065  coi2  6265  funprg  6594  funtpg  6595  funcnvtp  6603  funcnvqp  6604  funimass1  6622  fimadmfoALT  6807  f1orescnv  6840  resdif  6846  fvmpt2  7005  fvmptnf  7016  fveqressseq  7079  oveq12  7429  cbvmpov  7515  ovmpog  7579  fvmpopr2d  7582  caofinvl  7725  eqopi  8037  el2mpocsbcl  8096  fmpoco  8106  mposn  8114  fsuppeqg  8193  supp0cosupp0  8225  imacosupp  8226  mpocurryd  8286  fvmpocurryd  8288  rdgsucmptf  8436  frsucmpt  8446  oevn0  8523  oa0r  8546  om1r  8551  oe1m  8553  omass  8588  oeoalem  8605  oeoa  8606  oeoe  8608  qseq12  8782  curf  8890  map0g  8912  xpcomco  9086  sbthlem4  9109  sbthlem5  9110  xpmapenlem  9163  phplem2  9220  unxpdomlem3  9249  funsnfsupp  9384  ordtypelem7  9518  ttrcltr  9717  cardennn  10064  dfac9  10215  alephsing  10354  axcc3  10516  ac6num  10557  konigthlem  10653  canthp1lem2  10738  ordpipq  11027  ltrnq  11064  addclprlem2  11102  mulclprlem  11104  prlem934  11118  prlem936  11132  mulcmpblnrlem  11155  addcnsr  11220  mulcnsr  11221  axcnre  11249  recex  11948  rpnnen1lem3  13107  rpnnen1lem5  13109  xaddpnf1  13356  xaddpnf2  13357  xaddmnf1  13358  xaddmnf2  13359  rexadd  13362  xnn0xaddcl  13365  xaddnemnf  13366  xaddnepnf  13367  xadddilem  13424  addmodlteq  14089  om2uzrani  14095  om2uzrdg  14099  seqf1olem2  14185  seqf1o  14186  modexp  14382  faclbnd4lem3  14439  hashunsng  14536  hashwrdn  14692  lsw1  14712  swrdfv  14796  swrdccat  14884  ccats1pfxeqbi  14891  revfv  14912  cshwsublen  14947  wrdlen2  15095  wrdl2exs2  15097  wwlktovf1  15110  relexp0  15176  relexpcnv  15188  shftcan1  15236  remul2  15297  immul2  15304  sumss  15890  geomulcvg  16045  fprodss  16115  binomfallfaclem2  16206  bpolylem  16214  ef0lem  16244  efieq1re  16367  rpnnen2lem1  16382  ruclem3  16401  dvdsnegb  16443  dvdscmul  16452  dvds2ln  16459  dvds2add  16460  dvds2sub  16461  gcdn0val  16668  rpmulgcd  16731  lcmn0val  16770  odzval  16969  pcval  17022  pcmpt  17070  prmreclem4  17097  1arithlem2  17102  vdwlem8  17166  ramcl2lem  17187  ramtcl  17188  ramtub  17190  ramcl2  17194  ramcl  17207  setsval  17345  prfcl  18377  curf1cl  18402  curfcl  18406  hofcl  18433  yonedalem4c  18451  psssdm  18756  chneq12  18788  grplactval  19252  mulgnn0gsum  19290  cntzval  19535  f1omvdco2  19662  pmtrfinv  19675  psgnunilem5  19708  odlem2  19753  gexlem2  19796  lsmvalx  19853  efgtval  19937  efgredlema  19954  vrgpval  19981  cyggex  20112  gsumcom2  20189  fincygsubgodd  20328  dvdsrtr  20598  rnghmval  20670  abvtrivd  21089  lmhmco  21318  reslmhm  21327  lvecinv  21391  zrhmulg  21815  znzrhval  21852  ocvval  21973  mplmon2  22370  subrgasclcl  22376  coe1fv  22524  coe1fzgsumdlem  22621  evl1gsumdlem  22674  mat1dimscm  22790  dmatid  22810  scmatdmat  22830  mavmul0g  22868  1marepvmarrepid  22890  mdetunilem2  22928  gsummatr01lem3  22972  gsummatr01  22974  smadiadetlem3  22983  matunitlindf  22996  m2cpminvid2lem  23072  chpdmatlem2  23157  isopn3  23384  cnpval  23554  ptbasfi  23900  dfac14  23937  cnmptkk  24002  xkofvcn  24003  cnmptk1p  24004  cnmptk2  24005  xkocnv  24133  flfval  24309  ptcmplem3  24373  ptcmpg  24376  tmdmulg  24411  prdsxmslem2  24848  subgnm2  24953  nmoval  25034  fsum2cn  25192  pcovalg  25333  isclmp  25418  cphnm  25514  tcphnmval  25550  ovolctb  25811  ioorcl  25898  uniioombllem2  25904  itg1addlem3  26019  itg1climres  26035  itg2uba  26064  itg2splitlem  26069  elcpn  26254  dvexp  26273  dvexp2  26274  rolle  26310  cmvth  26311  mvth  26312  dvlip  26313  dvlipcn  26314  dvlip2  26315  dveq0  26320  dv11cn  26321  lhop1lem  26333  lhop2  26335  lhop  26336  dvcvx  26340  ftc2ditglem  26365  itgsubstlem  26368  ig1pval  26494  elply2  26514  coeid2  26558  coemul  26571  taylthlem2  26701  ulmdvlem1  26727  mtest  26731  pserval2  26738  abelthlem1  26758  abelthlem3  26760  abelthlem8  26766  abelthlem9  26767  pige3ALT  26848  0cxp  26994  leibpi  27270  igamgam  27376  mule1  27475  bposlem5  27615  lgsval3  27642  lgsdinn0  27672  dchrvmasumlem1  27822  dchrisum0flblem1  27835  rpvmasum2  27839  padicval  27944  abssid  28627  abssnid  28629  axsegconlem1  29495  ax5seglem9  29515  axpasch  29519  axeuclidlem  29540  axcontlem2  29543  finsumvtxdg2ssteplem4  30129  usgr2wlkspthlem2  30344  crctcshlem4  30409  wwlknp  30432  wlkiswwlks2lem3  30460  wwlksnred  30481  wwlksnextproplem2  30499  usgrwwlks2on  30547  umgrwwlks2on  30548  clwlkclwwlklem2a  30589  clwwisshclwwsn  30607  clwwlknlbonbgr1  30630  clwwlkn1loopb  30634  clwwlkf  30638  clwwlkext2edg  30647  wwlksext2clwwlk  30648  erclwwlknsym  30661  erclwwlkntr  30662  clwwlknon1  30688  clwwlknonex2  30700  eupth2lem3lem3  30831  eucrct2eupth  30846  fusgreghash2wspv  30936  2clwwlk2clwwlklem  30947  2clwwlk2clwwlk  30951  numclwwlk1lem2f1  30958  grpoidinvlem4  31109  grpoinvval  31125  grpodivval  31137  ipval  31305  sspgval  31331  sspsval  31333  sspnval  31339  nmooval  31365  ipasslem1  31433  ipasslem4  31436  hial0  31704  hial02  31705  ocsh  31885  pjhval  31999  hosval  32342  homval  32343  hodval  32344  hfsval  32345  hfmval  32346  braval  32546  kbval  32556  eigvalval  32562  0hmop  32585  adj0  32596  lnopeq0i  32609  nmopcoi  32697  pjclem4  32801  pj3si  32809  hstoh  32834  strlem3a  32854  hstrlem3a  32862  mdexchi  32937  atcv0eq  32981  atcv1  32982  fpwrelmap  33325  cycpmco2lem4  33690  cycpmco2lem5  33691  fxpgaval  33728  smatfval  34427  measxun2  34843  measdivcst  34857  measdivcstALTV  34858  ddeval1  34867  ddeval0  34868  ballotlemfp1  35124  signswmnd  35186  signstfvneq0  35201  signstfvc  35203  ftc2re  35227  itgexpif  35235  bnj1128  35620  subfacp1lem3  35947  subfacp1lem5  35949  cvmlift2lem3  36070  msubco  36296  altopthsn  36726  ditgeq12d  37011  fnetr  37139  fnejoin2  37157  ttcsntrsucg  37310  bj-evalid  37997  finxpreclem3  38316  finxpreclem5  38318  finxpreclem6  38319  curunc  38525  poimirlem4  38542  poimirlem25  38563  mblfinlem2  38576  mblfinlem3  38577  mbfresfi  38584  itg2addnclem  38589  itg2addnc  38592  ftc1anclem5  38615  isbnd3  38718  bndss  38720  grposnOLD  38816  ghomco  38825  xrneq12  39334  lkrval  40145  pmapval  40814  polvalN  40962  watvalN  41050  ldilset  41166  ltrnset  41175  dilsetN  41210  trnsetN  41213  trlset  41218  trlval  41219  cdleme16b  41336  cdleme31fv1  41448  cdlemg1idlemN  41629  tgrpset  41802  tendoset  41816  erngset  41857  erngplus  41860  erngmul  41863  erngset-rN  41865  erngplus-rN  41868  dvaset  42062  dvaplusg  42066  dvamulr  42069  dvavadd  42072  dvavsca  42074  diafval  42088  dvhset  42138  dvhmulr  42143  dvhvadd  42149  dvhvsca  42158  docafvalN  42179  djafvalN  42191  dibfval  42198  dicfval  42232  dihfval  42288  dihval  42289  dihvalc  42290  dihvalb  42294  dochfval  42407  djhfval  42454  lcdval  42646  mapdfval  42684  mapdn0  42726  hvmapfval  42816  hdmap1fval  42853  hdmapfval  42884  hgmapfval  42943  fmpocos  43287  sn-it0e0  43467  zaddcomlem  43527  pw2f1ocnv  44043  hbtlem7  44126  relexp0a  44715  ntrclscls00  45065  dvconstbi  45317  expgrowth  45318  addrfv  45450  subrfv  45451  mulvfv  45452  refsum2cnlem1  46053  limcperiod  46639  cncfiooiccre  46904  dvbdfbdioolem1  46937  itgioocnicc  46986  fourierdlem73  47188  fourierdlem82  47197  fourierdlem94  47209  fourierdlem103  47218  fourierdlem104  47219  fourierdlem113  47228  sqwvfoura  47237  etransclem46  47289  nnfoctbdjlem  47464  ovn0  47575  smflim  47786  afveu  48222  afv2eu  48307  fvmptrabdm  48362  imasetpreimafvbijlemfo  48486  lighneallem3  48691  ppivalnnprm  48709  mogoldbblem  48817  fpprel2  48838  sbgoldbwt  48874  nnsum4primeseven  48897  nnsum4primesevenALTV  48898  bgoldbtbnd  48906  grimco  48986  cycl3grtri  49044  lmod0rng  49325  lmodvsmdi  49490  lincdifsn  49535  lcoel0  49539  islindeps2  49594  blenn0  49684  nn0sumshdiglemA  49730  itcoval0mpt  49777  rrx2plordisom  49834  nelsubclem  50174  aacllem  50938