Theorem sylan9eq 2140

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

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

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 1381  ax-gen 1383  ax-4 1445  ax-17 1464  ax-ext 2070

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

This theorem is referenced by:  sylan9req  2141  sylan9eqr  2142  difeq12  3113  uneq12  3149  ineq12  3196  ifeq12  3407  preq12  3521  prprc  3552  preq12b  3614  opeq12  3624  xpeq12  4457  nfimad  4783  coi2  4947  funimass1  5091  f1orescnv  5269  resdif  5275  oveq12  5661  cbvmpt2v  5728  ovmpt2g  5779  eqopi  5942  fmpt2co  5981  nnaordex  6286  map0g  6445  xpcomco  6542  xpmapenlem  6565  phplem3  6570  phplem4  6571  sbthlemi5  6670  addcmpblnq  6926  ltrnqg  6979  enq0ref  6992  addcmpblnq0  7002  distrlem4prl  7143  distrlem4pru  7144  recexgt0sr  7319  axcnre  7416  cnegexlem2  7658  cnegexlem3  7659  recexap  8122  frec2uzrand  9812  iseqeq3  9860  shftcan1  10268  remul2  10307  immul2  10314  ef0lem  10950  efieq1re  11061  dvdsnegb  11091  dvdscmul  11101  dvds2ln  11107  dvds2add  11108  dvds2sub  11109  gcdn0val  11231  rpmulgcd  11293  lcmval  11323  lcmn0val  11326