Theorem sylan9eq 2259

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

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

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  sylan9req  2260  sylan9eqr  2261  difeq12  3290  uneq12  3326  ineq12  3373  ifeq12  3592  preq12  3717  prprc  3748  preq12b  3817  opeq12  3827  xpeq12  4702  nfimad  5040  coi2  5208  funimass1  5360  f1orescnv  5550  resdif  5556  oveq12  5966  cbvmpov  6038  ovmpog  6093  fvmpopr2d  6095  eqopi  6271  fmpoco  6315  nnaordex  6627  map0g  6788  xpcomco  6936  xpmapenlem  6961  phplem3  6966  phplem4  6967  sbthlemi5  7078  addcmpblnq  7500  ltrnqg  7553  enq0ref  7566  addcmpblnq0  7576  distrlem4prl  7717  distrlem4pru  7718  recexgt0sr  7906  axcnre  8014  cnegexlem2  8268  cnegexlem3  8269  recexap  8746  xaddpnf2  9989  xaddmnf2  9991  rexadd  9994  xaddnemnf  9999  xaddnepnf  10000  xposdif  10024  frec2uzrand  10572  seqeq3  10619  seqf1oglem2  10687  seqf1og  10688  lsw1  11065  shftcan1  11220  remul2  11259  immul2  11266  fprodssdc  11976  ef0lem  12046  efieq1re  12158  dvdsnegb  12194  dvdscmul  12204  dvds2ln  12210  dvds2add  12211  dvds2sub  12212  gcdn0val  12357  rpmulgcd  12422  lcmval  12460  lcmn0val  12463  odzval  12639  pcmpt  12741  grpsubval  13453  mulgnn0gsum  13539  crngpropd  13876  opprringbg  13917  dvdsrtr  13938  isopn3  14672  dvexp  15258  dvexp2  15259  elply2  15282  lgsval3  15570  lgsdinn0  15600  incistruhgr  15761  subctctexmid  16078