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  3248  uneq12  3284  ineq12  3331  ifeq12  3550  preq12  3671  prprc  3702  preq12b  3770  opeq12  3780  xpeq12  4645  nfimad  4979  coi2  5145  funimass1  5293  f1orescnv  5477  resdif  5483  oveq12  5883  cbvmpov  5954  ovmpog  6008  eqopi  6172  fmpoco  6216  nnaordex  6528  map0g  6687  xpcomco  6825  xpmapenlem  6848  phplem3  6853  phplem4  6854  sbthlemi5  6959  addcmpblnq  7365  ltrnqg  7418  enq0ref  7431  addcmpblnq0  7441  distrlem4prl  7582  distrlem4pru  7583  recexgt0sr  7771  axcnre  7879  cnegexlem2  8132  cnegexlem3  8133  recexap  8609  xaddpnf2  9846  xaddmnf2  9848  rexadd  9851  xaddnemnf  9856  xaddnepnf  9857  xposdif  9881  frec2uzrand  10404  seqeq3  10449  shftcan1  10842  remul2  10881  immul2  10888  fprodssdc  11597  ef0lem  11667  efieq1re  11778  dvdsnegb  11814  dvdscmul  11824  dvds2ln  11830  dvds2add  11831  dvds2sub  11832  gcdn0val  11961  rpmulgcd  12026  lcmval  12062  lcmn0val  12065  odzval  12240  pcmpt  12340  grpsubval  12918  crngpropd  13216  opprringbg  13248  dvdsrtr  13268  isopn3  13595  dvexp  14145  dvexp2  14146  lgsval3  14389  lgsdinn0  14419  subctctexmid  14720