Theorem sylan9eq 2284

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 2249	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶)
4	1, 2, 3	syl2an 289	1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224

This theorem is referenced by:  sylan9req  2285  sylan9eqr  2286  difeq12  3320  uneq12  3356  ineq12  3403  ifeq12  3622  preq12  3750  prprc  3782  preq12b  3853  opeq12  3864  xpeq12  4744  nfimad  5085  coi2  5253  funimass1  5407  f1orescnv  5599  resdif  5605  oveq12  6027  cbvmpov  6101  ovmpog  6156  fvmpopr2d  6158  eqopi  6335  fmpoco  6381  nnaordex  6696  map0g  6857  xpcomco  7010  xpmapenlem  7035  phplem3  7040  phplem4  7041  sbthlemi5  7160  addcmpblnq  7587  ltrnqg  7640  enq0ref  7653  addcmpblnq0  7663  distrlem4prl  7804  distrlem4pru  7805  recexgt0sr  7993  axcnre  8101  cnegexlem2  8355  cnegexlem3  8356  recexap  8833  xaddpnf2  10082  xaddmnf2  10084  rexadd  10087  xaddnemnf  10092  xaddnepnf  10093  xposdif  10117  frec2uzrand  10668  seqeq3  10715  seqf1oglem2  10783  seqf1og  10784  lsw1  11167  swrdccat  11320  ccats1pfxeqbi  11327  shftcan1  11412  remul2  11451  immul2  11458  fprodssdc  12169  ef0lem  12239  efieq1re  12351  dvdsnegb  12387  dvdscmul  12397  dvds2ln  12403  dvds2add  12404  dvds2sub  12405  gcdn0val  12550  rpmulgcd  12615  lcmval  12653  lcmn0val  12656  odzval  12832  pcmpt  12934  grpsubval  13647  mulgnn0gsum  13733  crngpropd  14071  opprringbg  14112  dvdsrtr  14134  isopn3  14868  dvexp  15454  dvexp2  15455  elply2  15478  lgsval3  15766  lgsdinn0  15796  incistruhgr  15960  clwwlkn1loopb  16290  clwwlkext2edg  16292  clwwlknonex2  16309  eupth2lem3lem3fi  16340  subctctexmid  16652