Theorem sylan9eq 2405

Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
sylan9eq.1	⊢ (φ → A = B)
sylan9eq.2	⊢ (ψ → B = C)

Assertion

Ref	Expression
sylan9eq	⊢ ((φ ∧ ψ) → A = C)

Proof of Theorem sylan9eq

Step	Hyp	Ref	Expression
1		sylan9eq.1	. 2 ⊢ (φ → A = B)
2		sylan9eq.2	. 2 ⊢ (ψ → B = C)
3		eqtr 2370	. 2 ⊢ ((A = B ∧ B = C) → A = C)
4	1, 2, 3	syl2an 463	1 ⊢ ((φ ∧ ψ) → A = C)

Syntax hints:   → wi 4   ∧ wa 358   = wceq 1642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-cleq 2346

This theorem is referenced by:  sylan9req  2406  sylan9eqr  2407  nineq12  3237  symdifeq12  3251  difeq12  3381  uneq12  3414  ineq12  3453  ifeq12  3676  ifbi  3680  preq12  3802  opkeq12  4062  preq12b  4128  xpkeq12  4201  addceq12  4386  opeq12  4581  xpeq12  4804  nfimad  4955  funimass1  5170  f1orescnv  5302  resdif  5307  oveq12  5533  caovmo  5646  cbvmpt2v  5681  fvmpt2  5705  ovmpt2g  5716  fvmptnf  5724  map0  6026  enmap2lem5  6068  enmap1lem3  6072  enmap1lem5  6074