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	|- ( ph -> A = B )
sylan9eq.2	|- ( ps -> B = C )

Assertion

Ref	Expression
sylan9eq	|- ( ( ph /\ ps ) -> A = C )

Proof of Theorem sylan9eq

Step	Hyp	Ref	Expression
1		sylan9eq.1	. 2 |- ( ph -> A = B )
2		sylan9eq.2	. 2 |- ( ps -> B = C )
3		eqtr 2256	. 2 |- ( ( A = B /\ B = C ) -> A = C )
4	1, 2, 3	syl2an 289	1 |- ( ( ph /\ ps ) -> A = C )

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  4795  nfimad  5138  coi2  5307  funimass1  5461  f1orescnv  5658  resdif  5664  oveq12  6097  cbvmpov  6171  ovmpog  6226  fvmpopr2d  6228  eqopi  6410  fmpoco  6456  supp0cosupp0fn  6511  imacosuppfn  6512  nnaordex  6805  map0g  6973  xpcomco  7128  xpmapenlem  7153  phplem3  7159  phplem4  7160  sbthlemi5  7283  addcmpblnq  7740  ltrnqg  7793  enq0ref  7806  addcmpblnq0  7816  distrlem4prl  7957  distrlem4pru  7958  recexgt0sr  8146  axcnre  8254  cnegexlem2  8509  cnegexlem3  8510  recexap  8989  xaddpnf2  10266  xaddmnf2  10268  rexadd  10271  xaddnemnf  10276  xaddnepnf  10277  xposdif  10301  frec2uzrand  10863  seqeq3  10910  seqf1oglem2  10978  seqf1og  10979  lsw1  11376  swrdccat  11529  ccats1pfxeqbi  11536  shftcan1  11621  remul2  11660  immul2  11667  fprodssdc  12382  ef0lem  12452  efieq1re  12564  dvdsnegb  12600  dvdscmul  12610  dvds2ln  12616  dvds2add  12617  dvds2sub  12618  gcdn0val  12763  rpmulgcd  12828  lcmval  12866  lcmn0val  12869  odzval  13049  pcmpt  13151  ballotfilemfp1  13289  grpsubval  13910  mulgnn0gzsum  13990  gsumcom2fi  14275  crngpropd  14451  opprringbg  14494  dvdsrtr  14517  isopn3  15351  dvexp  15937  dvexp2  15938  elply2  15961  bposlem5  16315  lgsval3  16342  lgsdinn0  16372  incistruhgr  16536  clwwlkn1loopb  16866  clwwlkext2edg  16868  clwwlknonex2  16885  eupth2lem3lem3fi  16916  subctctexmid  17235