Theorem sylan9eq 2285

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 2250	. 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 2214

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

This theorem is referenced by:  sylan9req  2286  sylan9eqr  2287  difeq12  3332  uneq12  3368  ineq12  3417  ifeq12  3639  preq12  3770  prprc  3802  preq12b  3874  opeq12  3885  xpeq12  4768  nfimad  5110  coi2  5279  funimass1  5433  f1orescnv  5630  resdif  5636  oveq12  6059  cbvmpov  6133  ovmpog  6188  fvmpopr2d  6190  eqopi  6366  fmpoco  6412  supp0cosupp0fn  6467  imacosuppfn  6468  nnaordex  6761  map0g  6922  xpcomco  7077  xpmapenlem  7102  phplem3  7108  phplem4  7109  sbthlemi5  7231  addcmpblnq  7682  ltrnqg  7735  enq0ref  7748  addcmpblnq0  7758  distrlem4prl  7899  distrlem4pru  7900  recexgt0sr  8088  axcnre  8196  cnegexlem2  8449  cnegexlem3  8450  recexap  8927  xaddpnf2  10180  xaddmnf2  10182  rexadd  10185  xaddnemnf  10190  xaddnepnf  10191  xposdif  10215  frec2uzrand  10767  seqeq3  10814  seqf1oglem2  10882  seqf1og  10883  lsw1  11274  swrdccat  11427  ccats1pfxeqbi  11434  shftcan1  11519  remul2  11558  immul2  11565  fprodssdc  12276  ef0lem  12346  efieq1re  12458  dvdsnegb  12494  dvdscmul  12504  dvds2ln  12510  dvds2add  12511  dvds2sub  12512  gcdn0val  12657  rpmulgcd  12722  lcmval  12760  lcmn0val  12763  odzval  12939  pcmpt  13041  grpsubval  13759  mulgnn0gsum  13845  crngpropd  14183  opprringbg  14224  dvdsrtr  14246  isopn3  14990  dvexp  15576  dvexp2  15577  elply2  15600  lgsval3  15891  lgsdinn0  15921  incistruhgr  16085  clwwlkn1loopb  16415  clwwlkext2edg  16417  clwwlknonex2  16434  eupth2lem3lem3fi  16465  subctctexmid  16774