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  10667  seqeq3  10714  seqf1oglem2  10782  seqf1og  10783  lsw1  11163  swrdccat  11316  ccats1pfxeqbi  11323  shftcan1  11395  remul2  11434  immul2  11441  fprodssdc  12152  ef0lem  12222  efieq1re  12334  dvdsnegb  12370  dvdscmul  12380  dvds2ln  12386  dvds2add  12387  dvds2sub  12388  gcdn0val  12533  rpmulgcd  12598  lcmval  12636  lcmn0val  12639  odzval  12815  pcmpt  12917  grpsubval  13630  mulgnn0gsum  13716  crngpropd  14054  opprringbg  14095  dvdsrtr  14117  isopn3  14851  dvexp  15437  dvexp2  15438  elply2  15461  lgsval3  15749  lgsdinn0  15779  incistruhgr  15943  clwwlkn1loopb  16273  clwwlkext2edg  16275  clwwlknonex2  16292  subctctexmid  16604