Theorem sylan9eq 2193

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

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133

This theorem is referenced by:  sylan9req  2194  sylan9eqr  2195  difeq12  3194  uneq12  3230  ineq12  3277  ifeq12  3493  preq12  3610  prprc  3641  preq12b  3705  opeq12  3715  xpeq12  4566  nfimad  4898  coi2  5063  funimass1  5208  f1orescnv  5391  resdif  5397  oveq12  5791  cbvmpov  5859  ovmpog  5913  eqopi  6078  fmpoco  6121  nnaordex  6431  map0g  6590  xpcomco  6728  xpmapenlem  6751  phplem3  6756  phplem4  6757  sbthlemi5  6857  addcmpblnq  7199  ltrnqg  7252  enq0ref  7265  addcmpblnq0  7275  distrlem4prl  7416  distrlem4pru  7417  recexgt0sr  7605  axcnre  7713  cnegexlem2  7962  cnegexlem3  7963  recexap  8438  xaddpnf2  9660  xaddmnf2  9662  rexadd  9665  xaddnemnf  9670  xaddnepnf  9671  xposdif  9695  frec2uzrand  10209  seqeq3  10254  shftcan1  10638  remul2  10677  immul2  10684  ef0lem  11403  efieq1re  11514  dvdsnegb  11546  dvdscmul  11556  dvds2ln  11562  dvds2add  11563  dvds2sub  11564  gcdn0val  11686  rpmulgcd  11750  lcmval  11780  lcmn0val  11783  isopn3  12333  dvexp  12883  dvexp2  12884  subctctexmid  13369