Theorem sylan9eq 2218

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

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  sylan9req  2219  sylan9eqr  2220  difeq12  3234  uneq12  3270  ineq12  3317  ifeq12  3535  preq12  3654  prprc  3685  preq12b  3749  opeq12  3759  xpeq12  4622  nfimad  4954  coi2  5119  funimass1  5264  f1orescnv  5447  resdif  5453  oveq12  5850  cbvmpov  5918  ovmpog  5972  eqopi  6137  fmpoco  6180  nnaordex  6491  map0g  6650  xpcomco  6788  xpmapenlem  6811  phplem3  6816  phplem4  6817  sbthlemi5  6922  addcmpblnq  7304  ltrnqg  7357  enq0ref  7370  addcmpblnq0  7380  distrlem4prl  7521  distrlem4pru  7522  recexgt0sr  7710  axcnre  7818  cnegexlem2  8070  cnegexlem3  8071  recexap  8546  xaddpnf2  9779  xaddmnf2  9781  rexadd  9784  xaddnemnf  9789  xaddnepnf  9790  xposdif  9814  frec2uzrand  10336  seqeq3  10381  shftcan1  10772  remul2  10811  immul2  10818  fprodssdc  11527  ef0lem  11597  efieq1re  11708  dvdsnegb  11744  dvdscmul  11754  dvds2ln  11760  dvds2add  11761  dvds2sub  11762  gcdn0val  11890  rpmulgcd  11955  lcmval  11991  lcmn0val  11994  odzval  12169  pcmpt  12269  isopn3  12725  dvexp  13275  dvexp2  13276  lgsval3  13519  lgsdinn0  13549  subctctexmid  13841