Theorem sylan9eq 2249

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

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

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  sylan9req  2250  sylan9eqr  2251  difeq12  3277  uneq12  3313  ineq12  3360  ifeq12  3578  preq12  3702  prprc  3733  preq12b  3801  opeq12  3811  xpeq12  4683  nfimad  5019  coi2  5187  funimass1  5336  f1orescnv  5523  resdif  5529  oveq12  5934  cbvmpov  6006  ovmpog  6061  fvmpopr2d  6063  eqopi  6239  fmpoco  6283  nnaordex  6595  map0g  6756  xpcomco  6894  xpmapenlem  6919  phplem3  6924  phplem4  6925  sbthlemi5  7036  addcmpblnq  7453  ltrnqg  7506  enq0ref  7519  addcmpblnq0  7529  distrlem4prl  7670  distrlem4pru  7671  recexgt0sr  7859  axcnre  7967  cnegexlem2  8221  cnegexlem3  8222  recexap  8699  xaddpnf2  9941  xaddmnf2  9943  rexadd  9946  xaddnemnf  9951  xaddnepnf  9952  xposdif  9976  frec2uzrand  10516  seqeq3  10563  seqf1oglem2  10631  seqf1og  10632  shftcan1  11018  remul2  11057  immul2  11064  fprodssdc  11774  ef0lem  11844  efieq1re  11956  dvdsnegb  11992  dvdscmul  12002  dvds2ln  12008  dvds2add  12009  dvds2sub  12010  gcdn0val  12155  rpmulgcd  12220  lcmval  12258  lcmn0val  12261  odzval  12437  pcmpt  12539  grpsubval  13250  mulgnn0gsum  13336  crngpropd  13673  opprringbg  13714  dvdsrtr  13735  isopn3  14469  dvexp  15055  dvexp2  15056  elply2  15079  lgsval3  15367  lgsdinn0  15397  subctctexmid  15755