Theorem sylan9eq 2106

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

Syntax hints:   → wi 4   ∧ wa 101   = wceq 1257

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1350  ax-gen 1352  ax-4 1414  ax-17 1433  ax-ext 2036

This theorem depends on definitions:  df-bi 114  df-cleq 2047

This theorem is referenced by:  sylan9req  2107  sylan9eqr  2108  difeq12  3082  uneq12  3117  ineq12  3158  ifeq12  3369  preq12  3474  prprc  3505  preq12b  3566  opeq12  3576  xpeq12  4389  nfimad  4702  coi2  4862  funimass1  5001  f1orescnv  5167  resdif  5173  oveq12  5546  cbvmpt2v  5609  ovmpt2g  5660  eqopi  5823  fmpt2co  5862  nnaordex  6128  xpcomco  6328  phplem3  6345  phplem4  6346  addcmpblnq  6493  ltrnqg  6546  enq0ref  6559  addcmpblnq0  6569  distrlem4prl  6710  distrlem4pru  6711  recexgt0sr  6886  axcnre  6983  cnegexlem2  7220  cnegexlem3  7221  recexap  7678  frec2uzzd  9315  frec2uzrand  9320  iseqeq3  9345  shftcan1  9627  remul2  9665  immul2  9672  dvdsnegb  10088  dvdscmul  10097  dvds2ln  10103  dvds2add  10104  dvds2sub  10105