Theorem sylan9eq 2249

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

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

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  sylan9req  2250  sylan9eqr  2251  difeq12  3277  uneq12  3313  ineq12  3360  ifeq12  3578  preq12  3702  prprc  3733  preq12b  3801  opeq12  3811  xpeq12  4683  nfimad  5019  coi2  5187  funimass1  5336  f1orescnv  5521  resdif  5527  oveq12  5932  cbvmpov  6003  ovmpog  6058  fvmpopr2d  6060  eqopi  6231  fmpoco  6275  nnaordex  6587  map0g  6748  xpcomco  6886  xpmapenlem  6911  phplem3  6916  phplem4  6917  sbthlemi5  7028  addcmpblnq  7436  ltrnqg  7489  enq0ref  7502  addcmpblnq0  7512  distrlem4prl  7653  distrlem4pru  7654  recexgt0sr  7842  axcnre  7950  cnegexlem2  8204  cnegexlem3  8205  recexap  8682  xaddpnf2  9924  xaddmnf2  9926  rexadd  9929  xaddnemnf  9934  xaddnepnf  9935  xposdif  9959  frec2uzrand  10499  seqeq3  10546  seqf1oglem2  10614  seqf1og  10615  shftcan1  11001  remul2  11040  immul2  11047  fprodssdc  11757  ef0lem  11827  efieq1re  11939  dvdsnegb  11975  dvdscmul  11985  dvds2ln  11991  dvds2add  11992  dvds2sub  11993  gcdn0val  12138  rpmulgcd  12203  lcmval  12241  lcmn0val  12244  odzval  12420  pcmpt  12522  grpsubval  13188  mulgnn0gsum  13268  crngpropd  13605  opprringbg  13646  dvdsrtr  13667  isopn3  14371  dvexp  14957  dvexp2  14958  elply2  14981  lgsval3  15269  lgsdinn0  15299  subctctexmid  15655