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  3777  preq12b  3848  opeq12  3859  xpeq12  4738  nfimad  5077  coi2  5245  funimass1  5398  f1orescnv  5590  resdif  5596  oveq12  6016  cbvmpov  6090  ovmpog  6145  fvmpopr2d  6147  eqopi  6324  fmpoco  6368  nnaordex  6682  map0g  6843  xpcomco  6993  xpmapenlem  7018  phplem3  7023  phplem4  7024  sbthlemi5  7139  addcmpblnq  7565  ltrnqg  7618  enq0ref  7631  addcmpblnq0  7641  distrlem4prl  7782  distrlem4pru  7783  recexgt0sr  7971  axcnre  8079  cnegexlem2  8333  cnegexlem3  8334  recexap  8811  xaddpnf2  10055  xaddmnf2  10057  rexadd  10060  xaddnemnf  10065  xaddnepnf  10066  xposdif  10090  frec2uzrand  10639  seqeq3  10686  seqf1oglem2  10754  seqf1og  10755  lsw1  11134  swrdccat  11282  ccats1pfxeqbi  11289  shftcan1  11360  remul2  11399  immul2  11406  fprodssdc  12116  ef0lem  12186  efieq1re  12298  dvdsnegb  12334  dvdscmul  12344  dvds2ln  12350  dvds2add  12351  dvds2sub  12352  gcdn0val  12497  rpmulgcd  12562  lcmval  12600  lcmn0val  12603  odzval  12779  pcmpt  12881  grpsubval  13594  mulgnn0gsum  13680  crngpropd  14017  opprringbg  14058  dvdsrtr  14080  isopn3  14814  dvexp  15400  dvexp2  15401  elply2  15424  lgsval3  15712  lgsdinn0  15742  incistruhgr  15905  subctctexmid  16425