Theorem sylan9eq 2210

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

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1335

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-cleq 2150

This theorem is referenced by:  sylan9req  2211  sylan9eqr  2212  difeq12  3220  uneq12  3256  ineq12  3303  ifeq12  3521  preq12  3638  prprc  3669  preq12b  3733  opeq12  3743  xpeq12  4605  nfimad  4937  coi2  5102  funimass1  5247  f1orescnv  5430  resdif  5436  oveq12  5833  cbvmpov  5901  ovmpog  5955  eqopi  6120  fmpoco  6163  nnaordex  6474  map0g  6633  xpcomco  6771  xpmapenlem  6794  phplem3  6799  phplem4  6800  sbthlemi5  6905  addcmpblnq  7287  ltrnqg  7340  enq0ref  7353  addcmpblnq0  7363  distrlem4prl  7504  distrlem4pru  7505  recexgt0sr  7693  axcnre  7801  cnegexlem2  8051  cnegexlem3  8052  recexap  8527  xaddpnf2  9751  xaddmnf2  9753  rexadd  9756  xaddnemnf  9761  xaddnepnf  9762  xposdif  9786  frec2uzrand  10304  seqeq3  10349  shftcan1  10734  remul2  10773  immul2  10780  fprodssdc  11487  ef0lem  11557  efieq1re  11668  dvdsnegb  11704  dvdscmul  11714  dvds2ln  11720  dvds2add  11721  dvds2sub  11722  gcdn0val  11845  rpmulgcd  11910  lcmval  11940  lcmn0val  11943  odzval  12116  isopn3  12536  dvexp  13086  dvexp2  13087  subctctexmid  13584