Theorem sylan9eq 2284

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  sylan9req  2285  sylan9eqr  2286  difeq12  3322  uneq12  3358  ineq12  3405  ifeq12  3626  preq12  3754  prprc  3786  preq12b  3858  opeq12  3869  xpeq12  4750  nfimad  5091  coi2  5260  funimass1  5414  f1orescnv  5608  resdif  5614  oveq12  6037  cbvmpov  6111  ovmpog  6166  fvmpopr2d  6168  eqopi  6344  fmpoco  6390  supp0cosupp0fn  6445  imacosuppfn  6446  nnaordex  6739  map0g  6900  xpcomco  7053  xpmapenlem  7078  phplem3  7083  phplem4  7084  sbthlemi5  7203  addcmpblnq  7630  ltrnqg  7683  enq0ref  7696  addcmpblnq0  7706  distrlem4prl  7847  distrlem4pru  7848  recexgt0sr  8036  axcnre  8144  cnegexlem2  8397  cnegexlem3  8398  recexap  8875  xaddpnf2  10126  xaddmnf2  10128  rexadd  10131  xaddnemnf  10136  xaddnepnf  10137  xposdif  10161  frec2uzrand  10713  seqeq3  10760  seqf1oglem2  10828  seqf1og  10829  lsw1  11212  swrdccat  11365  ccats1pfxeqbi  11372  shftcan1  11457  remul2  11496  immul2  11503  fprodssdc  12214  ef0lem  12284  efieq1re  12396  dvdsnegb  12432  dvdscmul  12442  dvds2ln  12448  dvds2add  12449  dvds2sub  12450  gcdn0val  12595  rpmulgcd  12660  lcmval  12698  lcmn0val  12701  odzval  12877  pcmpt  12979  grpsubval  13692  mulgnn0gsum  13778  crngpropd  14116  opprringbg  14157  dvdsrtr  14179  isopn3  14919  dvexp  15505  dvexp2  15506  elply2  15529  lgsval3  15820  lgsdinn0  15850  incistruhgr  16014  clwwlkn1loopb  16344  clwwlkext2edg  16346  clwwlknonex2  16363  eupth2lem3lem3fi  16394  subctctexmid  16705