Theorem sylan9eqr 2091

Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.)

Hypotheses

Ref	Expression
sylan9eqr.1	|- (ph -> A = B)
sylan9eqr.2	|- (ps -> B = C)

Assertion

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

Proof of Theorem sylan9eqr

Step	Hyp	Ref	Expression
1		sylan9eqr.1	. . 3 |- (ph -> A = B)
2		sylan9eqr.2	. . 3 |- (ps -> B = C)
3	1, 2	sylan9eq 2089	. 2 |- ((ph /\ ps) -> A = C)
4	3	ancoms 255	1 |- ((ps /\ ph) -> A = C)

Syntax hints:   -> wi 4   /\ wa 97   = wceq 1242

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-cleq 2030

This theorem is referenced by:  sbcied2  2794  csbied2  2887  fun2ssres  4886  fcoi1  5013  fcoi2  5014  funssfv  5142  caovimo  5636  mpt2mptsx  5765  dmmpt2ssx  5767  fmpt2x  5768  2ndconst  5785  mpt2xopoveq  5796  tfrlemisucaccv  5880  rdgivallem  5908  nnmass  6005  nnm00  6038  ltexnqq  6391  ltrnqg  6403  nqnq0a  6437  nqnq0m  6438  nq0m0r  6439  nq0a0  6440  addnqprllem  6510  addnqprulem  6511  nnnn0addcl  7988  zindd  8132  qaddcl  8346  qmulcl  8348  qreccl  8351  frec2uzrdg  8876  expp1  8916  expnegap0  8917  expcllem  8920  mulexp  8948  expmul  8954  reim0b  9090  cjexp  9121