Theorem sylan9eq 2246

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 2211	. 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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186

This theorem is referenced by:  sylan9req  2247  sylan9eqr  2248  difeq12  3272  uneq12  3308  ineq12  3355  ifeq12  3573  preq12  3697  prprc  3728  preq12b  3796  opeq12  3806  xpeq12  4678  nfimad  5014  coi2  5182  funimass1  5331  f1orescnv  5516  resdif  5522  oveq12  5927  cbvmpov  5998  ovmpog  6053  eqopi  6225  fmpoco  6269  nnaordex  6581  map0g  6742  xpcomco  6880  xpmapenlem  6905  phplem3  6910  phplem4  6911  sbthlemi5  7020  addcmpblnq  7427  ltrnqg  7480  enq0ref  7493  addcmpblnq0  7503  distrlem4prl  7644  distrlem4pru  7645  recexgt0sr  7833  axcnre  7941  cnegexlem2  8195  cnegexlem3  8196  recexap  8672  xaddpnf2  9913  xaddmnf2  9915  rexadd  9918  xaddnemnf  9923  xaddnepnf  9924  xposdif  9948  frec2uzrand  10476  seqeq3  10523  seqf1oglem2  10591  seqf1og  10592  shftcan1  10978  remul2  11017  immul2  11024  fprodssdc  11733  ef0lem  11803  efieq1re  11915  dvdsnegb  11951  dvdscmul  11961  dvds2ln  11967  dvds2add  11968  dvds2sub  11969  gcdn0val  12098  rpmulgcd  12163  lcmval  12201  lcmn0val  12204  odzval  12379  pcmpt  12481  grpsubval  13118  mulgnn0gsum  13198  crngpropd  13535  opprringbg  13576  dvdsrtr  13597  isopn3  14293  dvexp  14860  dvexp2  14861  elply2  14881  lgsval3  15134  lgsdinn0  15164  subctctexmid  15491