Theorem sylan9eq 2291

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  sylan9req  2292  sylan9eqr  2293  difeq12  3342  uneq12  3378  ineq12  3427  ifeq12  3657  preq12  3790  prprc  3823  preq12b  3895  opeq12  3906  xpeq12  4793  nfimad  5135  coi2  5304  funimass1  5458  f1orescnv  5655  resdif  5661  oveq12  6094  cbvmpov  6168  ovmpog  6223  fvmpopr2d  6225  eqopi  6406  fmpoco  6452  supp0cosupp0fn  6507  imacosuppfn  6508  nnaordex  6801  map0g  6969  xpcomco  7124  xpmapenlem  7149  phplem3  7155  phplem4  7156  sbthlemi5  7278  addcmpblnq  7734  ltrnqg  7787  enq0ref  7800  addcmpblnq0  7810  distrlem4prl  7951  distrlem4pru  7952  recexgt0sr  8140  axcnre  8248  cnegexlem2  8503  cnegexlem3  8504  recexap  8983  xaddpnf2  10259  xaddmnf2  10261  rexadd  10264  xaddnemnf  10269  xaddnepnf  10270  xposdif  10294  frec2uzrand  10855  seqeq3  10902  seqf1oglem2  10970  seqf1og  10971  lsw1  11368  swrdccat  11521  ccats1pfxeqbi  11528  shftcan1  11613  remul2  11652  immul2  11659  fprodssdc  12373  ef0lem  12443  efieq1re  12555  dvdsnegb  12591  dvdscmul  12601  dvds2ln  12607  dvds2add  12608  dvds2sub  12609  gcdn0val  12754  rpmulgcd  12819  lcmval  12857  lcmn0val  12860  odzval  13040  pcmpt  13142  ballotfilemfp1  13280  grpsubval  13900  mulgnn0gzsum  13980  crngpropd  14393  opprringbg  14434  dvdsrtr  14457  isopn3  15275  dvexp  15861  dvexp2  15862  elply2  15885  bposlem5  16213  lgsval3  16235  lgsdinn0  16265  incistruhgr  16429  clwwlkn1loopb  16759  clwwlkext2edg  16761  clwwlknonex2  16778  eupth2lem3lem3fi  16809  subctctexmid  17128