Theorem sylan9eqr 2293

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 2291	. 2 |- ( ( ph /\ ps ) -> A = C )
4	3	ancoms 268	1 |- ( ( ps /\ ph ) -> 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:  sbcied2  3089  csbied2  3195  fun2ssres  5424  fcoi1  5575  fcoi2  5576  funssfv  5724  caovimo  6286  mpomptsx  6437  dmmpossx  6439  fmpox  6440  2ndconst  6462  mpoxopoveq  6516  tfrlemisucaccv  6601  tfr1onlemsucaccv  6617  tfrcllemsucaccv  6630  rdgivallem  6657  nnmass  6765  nnm00  6808  mapsnend  7105  ssenen  7158  fi0  7314  nnnninf2  7473  nnnninfeq2  7475  exmidfodomrlemim  7559  ltexnqq  7781  ltrnqg  7793  nqnq0a  7827  nqnq0m  7828  nq0m0r  7829  nq0a0  7830  addnqprllem  7900  addnqprulem  7901  map2psrprg  8178  rereceu  8262  addid0  8706  nnnn0addcl  9604  zindd  9774  qaddcl  10050  qmulcl  10052  qreccl  10057  xaddpnf1  10264  xaddmnf1  10266  xaddnemnf  10275  xaddnepnf  10276  xaddcom  10279  xnegdi  10286  xaddass  10287  xpncan  10289  xleadd1a  10291  xltadd1  10294  xlt2add  10298  modfzo0difsn  10852  frec2uzrdg  10866  seqf1oglem2  10977  expp1  11003  expnegap0  11004  expcllem  11007  mulexp  11035  expmul  11041  sqoddm1div8  11151  bcpasc  11225  hashfzo  11284  hashf1lem1  11306  lsw0  11373  ccatval1  11386  ccatval2  11387  swrdval  11441  ccatopth  11509  reuccatpfxs1  11540  shftfn  11610  reim0b  11648  cjexp  11679  sumsnf  12200  binomlem  12274  prodsnf  12383  ef0lem  12451  dvdsnegb  12599  m1expe  12690  m1expo  12691  m1exp1  12692  flodddiv4  12727  gcdabs  12789  bezoutr1  12834  dvdslcm  12871  lcmeq0  12873  lcmcl  12874  lcmabs  12878  lcmgcdlem  12879  lcmdvds  12881  mulgcddvds  12896  qredeu  12899  divgcdcoprmex  12904  pcge0  13120  pcgcd1  13135  pcadd  13147  pcmpt2  13151  mulgfvalg  13982  mulgnn0subcl  13996  mulgnn0z  14010  f1ghm0to0  14133  gsumresfi  14262  srgmulgass  14399  srgpcomp  14400  ringinvnzdiv  14461  lmodvsmmulgdi  14768  znval  15079  assamulgscmlem2  15150  mplvalg  15222  isxmet2d  15591  blfvalps  15628  blssioo  15796  efper  16051  relogbcxpbap  16218  logbgcd1irr  16220  zprmlogbaplem2  16233  chtqub  16313  bposlem2  16329  lgsdir  16376  lgsne0  16379  lgsdirnn0  16388  lgsdinn0  16389  lgsquadlem2  16419  2lgslem3a  16434  2lgslem3b  16435  2lgslem3c  16436  2lgslem3d  16437  2lgslem3a1  16438  2lgslem3b1  16439  2lgslem3c1  16440  2lgslem3d1  16441  wlklenvm1  16804  wlklenvm1g  16805  wlk0prc  16835  clwwlkn2  16884  trirec0xor  17318