Theorem sylan9eq 2282

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

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

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  sylan9req  2283  sylan9eqr  2284  difeq12  3318  uneq12  3354  ineq12  3401  ifeq12  3620  preq12  3748  prprc  3780  preq12b  3851  opeq12  3862  xpeq12  4742  nfimad  5083  coi2  5251  funimass1  5404  f1orescnv  5596  resdif  5602  oveq12  6022  cbvmpov  6096  ovmpog  6151  fvmpopr2d  6153  eqopi  6330  fmpoco  6376  nnaordex  6691  map0g  6852  xpcomco  7005  xpmapenlem  7030  phplem3  7035  phplem4  7036  sbthlemi5  7151  addcmpblnq  7577  ltrnqg  7630  enq0ref  7643  addcmpblnq0  7653  distrlem4prl  7794  distrlem4pru  7795  recexgt0sr  7983  axcnre  8091  cnegexlem2  8345  cnegexlem3  8346  recexap  8823  xaddpnf2  10072  xaddmnf2  10074  rexadd  10077  xaddnemnf  10082  xaddnepnf  10083  xposdif  10107  frec2uzrand  10657  seqeq3  10704  seqf1oglem2  10772  seqf1og  10773  lsw1  11153  swrdccat  11306  ccats1pfxeqbi  11313  shftcan1  11385  remul2  11424  immul2  11431  fprodssdc  12141  ef0lem  12211  efieq1re  12323  dvdsnegb  12359  dvdscmul  12369  dvds2ln  12375  dvds2add  12376  dvds2sub  12377  gcdn0val  12522  rpmulgcd  12587  lcmval  12625  lcmn0val  12628  odzval  12804  pcmpt  12906  grpsubval  13619  mulgnn0gsum  13705  crngpropd  14042  opprringbg  14083  dvdsrtr  14105  isopn3  14839  dvexp  15425  dvexp2  15426  elply2  15449  lgsval3  15737  lgsdinn0  15767  incistruhgr  15931  clwwlkn1loopb  16215  clwwlkext2edg  16217  clwwlknonex2  16234  subctctexmid  16537