Theorem sylan9eq 2257

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

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

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  sylan9req  2258  sylan9eqr  2259  difeq12  3285  uneq12  3321  ineq12  3368  ifeq12  3586  preq12  3711  prprc  3742  preq12b  3810  opeq12  3820  xpeq12  4693  nfimad  5030  coi2  5198  funimass1  5350  f1orescnv  5537  resdif  5543  oveq12  5952  cbvmpov  6024  ovmpog  6079  fvmpopr2d  6081  eqopi  6257  fmpoco  6301  nnaordex  6613  map0g  6774  xpcomco  6920  xpmapenlem  6945  phplem3  6950  phplem4  6951  sbthlemi5  7062  addcmpblnq  7479  ltrnqg  7532  enq0ref  7545  addcmpblnq0  7555  distrlem4prl  7696  distrlem4pru  7697  recexgt0sr  7885  axcnre  7993  cnegexlem2  8247  cnegexlem3  8248  recexap  8725  xaddpnf2  9968  xaddmnf2  9970  rexadd  9973  xaddnemnf  9978  xaddnepnf  9979  xposdif  10003  frec2uzrand  10548  seqeq3  10595  seqf1oglem2  10663  seqf1og  10664  lsw1  11041  shftcan1  11087  remul2  11126  immul2  11133  fprodssdc  11843  ef0lem  11913  efieq1re  12025  dvdsnegb  12061  dvdscmul  12071  dvds2ln  12077  dvds2add  12078  dvds2sub  12079  gcdn0val  12224  rpmulgcd  12289  lcmval  12327  lcmn0val  12330  odzval  12506  pcmpt  12608  grpsubval  13320  mulgnn0gsum  13406  crngpropd  13743  opprringbg  13784  dvdsrtr  13805  isopn3  14539  dvexp  15125  dvexp2  15126  elply2  15149  lgsval3  15437  lgsdinn0  15467  subctctexmid  15870