Theorem sylan9eq 2134

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

Syntax hints:   → wi 4   ∧ wa 102   = wceq 1285

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-cleq 2075

This theorem is referenced by:  sylan9req  2135  sylan9eqr  2136  difeq12  3086  uneq12  3122  ineq12  3163  ifeq12  3367  preq12  3473  prprc  3504  preq12b  3564  opeq12  3574  xpeq12  4384  nfimad  4701  coi2  4861  funimass1  5001  f1orescnv  5167  resdif  5173  oveq12  5546  cbvmpt2v  5609  ovmpt2g  5660  eqopi  5823  fmpt2co  5862  nnaordex  6159  xpcomco  6360  phplem3  6379  phplem4  6380  addcmpblnq  6608  ltrnqg  6661  enq0ref  6674  addcmpblnq0  6684  distrlem4prl  6825  distrlem4pru  6826  recexgt0sr  7001  axcnre  7098  cnegexlem2  7340  cnegexlem3  7341  recexap  7799  frec2uzrand  9476  iseqeq3  9515  shftcan1  9849  remul2  9887  immul2  9894  dvdsnegb  10346  dvdscmul  10356  dvds2ln  10362  dvds2add  10363  dvds2sub  10364  gcdn0val  10486  rpmulgcd  10548  lcmval  10578  lcmn0val  10581