Theorem sylan9eq 2282

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

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

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  sylan9req  2283  sylan9eqr  2284  difeq12  3317  uneq12  3353  ineq12  3400  ifeq12  3619  preq12  3745  prprc  3776  preq12b  3847  opeq12  3858  xpeq12  4737  nfimad  5076  coi2  5244  funimass1  5397  f1orescnv  5587  resdif  5593  oveq12  6009  cbvmpov  6083  ovmpog  6138  fvmpopr2d  6140  eqopi  6316  fmpoco  6360  nnaordex  6672  map0g  6833  xpcomco  6981  xpmapenlem  7006  phplem3  7011  phplem4  7012  sbthlemi5  7124  addcmpblnq  7550  ltrnqg  7603  enq0ref  7616  addcmpblnq0  7626  distrlem4prl  7767  distrlem4pru  7768  recexgt0sr  7956  axcnre  8064  cnegexlem2  8318  cnegexlem3  8319  recexap  8796  xaddpnf2  10039  xaddmnf2  10041  rexadd  10044  xaddnemnf  10049  xaddnepnf  10050  xposdif  10074  frec2uzrand  10622  seqeq3  10669  seqf1oglem2  10737  seqf1og  10738  lsw1  11116  swrdccat  11262  ccats1pfxeqbi  11269  shftcan1  11340  remul2  11379  immul2  11386  fprodssdc  12096  ef0lem  12166  efieq1re  12278  dvdsnegb  12314  dvdscmul  12324  dvds2ln  12330  dvds2add  12331  dvds2sub  12332  gcdn0val  12477  rpmulgcd  12542  lcmval  12580  lcmn0val  12583  odzval  12759  pcmpt  12861  grpsubval  13574  mulgnn0gsum  13660  crngpropd  13997  opprringbg  14038  dvdsrtr  14059  isopn3  14793  dvexp  15379  dvexp2  15380  elply2  15403  lgsval3  15691  lgsdinn0  15721  incistruhgr  15884  subctctexmid  16325