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  6806  map0g  6974  xpcomco  7130  xpmapenlem  7155  phplem3  7161  phplem4  7162  sbthlemi5  7285  addcmpblnq  7740  ltrnqg  7793  enq0ref  7806  addcmpblnq0  7816  distrlem4prl  7957  distrlem4pru  7958  recexgt0sr  8146  axcnre  8254  cnegexlem2  8509  cnegexlem3  8510  recexap  8989  xaddpnf2  10265  xaddmnf2  10267  rexadd  10270  xaddnemnf  10275  xaddnepnf  10276  xposdif  10300  frec2uzrand  10862  seqeq3  10909  seqf1oglem2  10977  seqf1og  10978  lsw1  11375  swrdccat  11528  ccats1pfxeqbi  11535  shftcan1  11620  remul2  11659  immul2  11666  fprodssdc  12381  ef0lem  12451  efieq1re  12563  dvdsnegb  12599  dvdscmul  12609  dvds2ln  12615  dvds2add  12616  dvds2sub  12617  gcdn0val  12762  rpmulgcd  12827  lcmval  12865  lcmn0val  12868  odzval  13048  pcmpt  13150  ballotfilemfp1  13288  grpsubval  13909  mulgnn0gzsum  13989  gsumcom2fi  14274  crngpropd  14450  opprringbg  14493  dvdsrtr  14516  isopn3  15368  dvexp  15954  dvexp2  15955  elply2  15978  bposlem5  16332  lgsval3  16359  lgsdinn0  16389  incistruhgr  16553  clwwlkn1loopb  16883  clwwlkext2edg  16885  clwwlknonex2  16902  eupth2lem3lem3fi  16933  subctctexmid  17252