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  3276  uneq12  3312  ineq12  3359  ifeq12  3577  preq12  3701  prprc  3732  preq12b  3800  opeq12  3810  xpeq12  4682  nfimad  5018  coi2  5186  funimass1  5335  f1orescnv  5520  resdif  5526  oveq12  5931  cbvmpov  6002  ovmpog  6057  fvmpopr2d  6059  eqopi  6230  fmpoco  6274  nnaordex  6586  map0g  6747  xpcomco  6885  xpmapenlem  6910  phplem3  6915  phplem4  6916  sbthlemi5  7027  addcmpblnq  7434  ltrnqg  7487  enq0ref  7500  addcmpblnq0  7510  distrlem4prl  7651  distrlem4pru  7652  recexgt0sr  7840  axcnre  7948  cnegexlem2  8202  cnegexlem3  8203  recexap  8680  xaddpnf2  9922  xaddmnf2  9924  rexadd  9927  xaddnemnf  9932  xaddnepnf  9933  xposdif  9957  frec2uzrand  10497  seqeq3  10544  seqf1oglem2  10612  seqf1og  10613  shftcan1  10999  remul2  11038  immul2  11045  fprodssdc  11755  ef0lem  11825  efieq1re  11937  dvdsnegb  11973  dvdscmul  11983  dvds2ln  11989  dvds2add  11990  dvds2sub  11991  gcdn0val  12128  rpmulgcd  12193  lcmval  12231  lcmn0val  12234  odzval  12410  pcmpt  12512  grpsubval  13178  mulgnn0gsum  13258  crngpropd  13595  opprringbg  13636  dvdsrtr  13657  isopn3  14361  dvexp  14947  dvexp2  14948  elply2  14971  lgsval3  15259  lgsdinn0  15289  subctctexmid  15645