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  6026  cbvmpov  6100  ovmpog  6155  fvmpopr2d  6157  eqopi  6334  fmpoco  6380  nnaordex  6695  map0g  6856  xpcomco  7009  xpmapenlem  7034  phplem3  7039  phplem4  7040  sbthlemi5  7159  addcmpblnq  7586  ltrnqg  7639  enq0ref  7652  addcmpblnq0  7662  distrlem4prl  7803  distrlem4pru  7804  recexgt0sr  7992  axcnre  8100  cnegexlem2  8354  cnegexlem3  8355  recexap  8832  xaddpnf2  10081  xaddmnf2  10083  rexadd  10086  xaddnemnf  10091  xaddnepnf  10092  xposdif  10116  frec2uzrand  10666  seqeq3  10713  seqf1oglem2  10781  seqf1og  10782  lsw1  11162  swrdccat  11315  ccats1pfxeqbi  11322  shftcan1  11394  remul2  11433  immul2  11440  fprodssdc  12150  ef0lem  12220  efieq1re  12332  dvdsnegb  12368  dvdscmul  12378  dvds2ln  12384  dvds2add  12385  dvds2sub  12386  gcdn0val  12531  rpmulgcd  12596  lcmval  12634  lcmn0val  12637  odzval  12813  pcmpt  12915  grpsubval  13628  mulgnn0gsum  13714  crngpropd  14051  opprringbg  14092  dvdsrtr  14114  isopn3  14848  dvexp  15434  dvexp2  15435  elply2  15458  lgsval3  15746  lgsdinn0  15776  incistruhgr  15940  clwwlkn1loopb  16270  clwwlkext2edg  16272  clwwlknonex2  16289  subctctexmid  16601