Theorem sylan9eq 2230

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

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

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  sylan9req  2231  sylan9eqr  2232  difeq12  3250  uneq12  3286  ineq12  3333  ifeq12  3552  preq12  3673  prprc  3704  preq12b  3772  opeq12  3782  xpeq12  4647  nfimad  4981  coi2  5147  funimass1  5295  f1orescnv  5479  resdif  5485  oveq12  5887  cbvmpov  5958  ovmpog  6012  eqopi  6176  fmpoco  6220  nnaordex  6532  map0g  6691  xpcomco  6829  xpmapenlem  6852  phplem3  6857  phplem4  6858  sbthlemi5  6963  addcmpblnq  7369  ltrnqg  7422  enq0ref  7435  addcmpblnq0  7445  distrlem4prl  7586  distrlem4pru  7587  recexgt0sr  7775  axcnre  7883  cnegexlem2  8136  cnegexlem3  8137  recexap  8613  xaddpnf2  9850  xaddmnf2  9852  rexadd  9855  xaddnemnf  9860  xaddnepnf  9861  xposdif  9885  frec2uzrand  10408  seqeq3  10453  shftcan1  10846  remul2  10885  immul2  10892  fprodssdc  11601  ef0lem  11671  efieq1re  11782  dvdsnegb  11818  dvdscmul  11828  dvds2ln  11834  dvds2add  11835  dvds2sub  11836  gcdn0val  11965  rpmulgcd  12030  lcmval  12066  lcmn0val  12069  odzval  12244  pcmpt  12344  grpsubval  12925  crngpropd  13224  opprringbg  13256  dvdsrtr  13276  isopn3  13765  dvexp  14315  dvexp2  14316  lgsval3  14559  lgsdinn0  14589  subctctexmid  14890