Theorem syl5eq 2184

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

Ref	Expression
syl5eq	|- ( ph -> A = C )

Proof of Theorem syl5eq

Step	Hyp	Ref	Expression
1		syl5eq.1	. . 3 |- A = B
2	1	a1i 9	. 2 |- ( ph -> A = B )
3		syl5eq.2	. 2 |- ( ph -> B = C )
4	2, 3	eqtrd 2172	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132

This theorem is referenced by:  syl5req  2185  syl5eqr  2186  3eqtr3a  2196  3eqtr4g  2197  csbtt  3014  csbvarg  3030  csbie2g  3050  rabbi2dva  3284  csbprc  3408  disjssun  3426  disjpr2  3587  prprc2  3632  difprsn2  3660  opprc  3726  intsng  3805  riinm  3885  iinxsng  3886  iunxprg  3893  rintm  3905  sucprc  4334  unisucg  4336  xpriindim  4677  relop  4689  dmxpm  4759  riinint  4800  resabs1  4848  resabs2  4850  resima2  4853  xpssres  4854  resopab2  4866  imasng  4904  ndmima  4916  xpdisj1  4963  xpdisj2  4964  djudisj  4966  resdisj  4967  rnxpm  4968  xpima1  4985  xpima2m  4986  dmsnsnsng  5016  rnsnopg  5017  rnpropg  5018  mptiniseg  5033  dfco2a  5039  relcoi1  5070  unixpm  5074  iotaval  5099  funtp  5176  fnun  5229  fnresdisj  5233  fnima  5241  fnimaeq0  5244  fcoi1  5303  f1orescnv  5383  foun  5386  resdif  5389  tz6.12-2  5412  fveu  5413  tz6.12-1  5448  fvun2  5488  fvopab3ig  5495  f1oresrab  5585  dfmptg  5599  ressnop0  5601  fvunsng  5614  fnsnsplitss  5619  fsnunfv  5621  fvpr1  5624  fvpr2  5625  fvpr1g  5626  fvpr2g  5627  fvtp1g  5628  fvtp2g  5629  fvtp3g  5630  fvtp2  5632  fvtp3  5633  f1oiso2  5728  riotaund  5764  ovprc  5806  resoprab2  5868  fnoprabg  5872  ovidig  5888  ovigg  5891  ov6g  5908  ovconst2  5922  offval2  5997  ot1stg  6050  ot2ndg  6051  ot3rdgg  6052  fmpoco  6113  algrflemg  6127  tpostpos2  6162  rdgisuc1  6281  frec0g  6294  frecsuclem  6303  frecrdg  6305  oasuc  6360  oa1suc  6363  omsuc  6368  nnm1  6420  nnm2  6421  dfec2  6432  errn  6451  ixpsnval  6595  ixpintm  6619  mapen  6740  xpmapenlem  6743  phplem2  6747  undifdc  6812  fisseneq  6820  ssfirab  6822  eqinfti  6907  infvalti  6909  infsnti  6917  casef  6973  caseinl  6976  caseinr  6977  djudom  6978  ctssdccl  6996  exmidfodomrlemim  7057  1qec  7196  mulidnq  7197  addpinq1  7272  suplocexprlem2b  7522  suplocexprlemlub  7532  0idsr  7575  1idsr  7576  caucvgsrlemoffres  7608  caucvgsr  7610  mulresr  7646  pitonnlem2  7655  ax1rid  7685  axcnre  7689  negid  8009  subneg  8011  negneg  8012  dfinfre  8714  2times  8848  infrenegsupex  9389  rexneg  9613  xaddpnf2  9630  xaddmnf1  9631  xaddmnf2  9632  fseq1p1m1  9874  fzosplitprm1  10011  intfracq  10093  frec2uz0d  10172  frec2uzrdg  10182  frecuzrdg0  10186  frecuzrdgg  10189  frecuzrdg0t  10195  seq3val  10231  seqvalcd  10232  iseqf1olemjpcl  10268  iseqf1olemqpcl  10269  iseqf1olemfvp  10270  seq3f1olemqsum  10273  sqval  10351  iexpcyc  10397  binom3  10409  faclbnd  10487  faclbnd2  10488  bcn1  10504  hashinfom  10524  hashennn  10526  hashxp  10572  shftlem  10588  shftuz  10589  shftidt  10605  reim0  10633  remullem  10643  resqrexlemf1  10780  resqrexlemcalc3  10788  absexpzap  10852  absimle  10856  amgm2  10890  minmax  11001  xrmaxiflemval  11019  xrmaxadd  11030  infxrnegsupex  11032  xrminmax  11034  summodc  11152  fsum3  11156  sumsnf  11178  sumsns  11184  isumclim3  11192  isumge0  11199  fsump1i  11202  fsum2dlemstep  11203  fisumcom2  11207  fsumshftm  11214  fsumconst  11223  fsumiun  11246  hashrabrex  11250  hashuni  11251  binom11  11255  isumsplit  11260  geo2sum  11283  mertensabs  11306  prodmodc  11347  efgt1p2  11401  efgt1p  11402  resinval  11422  recosval  11423  cosadd  11444  ef01bndlem  11463  eirraplem  11483  ialgr0  11725  algrp1  11727  eucalg  11740  phiprmpw  11898  phiprm  11899  ennnfonelem0  11918  ennnfonelemfun  11930  ennnfonelemf1  11931  ennnfonelemrn  11932  ctinfomlemom  11940  ndxid  11983  setsfun0  11995  setsresg  11997  setscom  11999  strslfv2d  12001  ressid2  12018  ressval2  12019  tgidm  12243  tgrest  12338  ssidcn  12379  txcnmpt  12442  txcn  12444  blres  12603  mopnval  12611  remetdval  12708  divccncfap  12746  cncfmet  12748  cncfcncntop  12749  cnplimcim  12805  cnplimclemr  12807  limccnpcntop  12813  limccnp2cntop  12815  dvexp  12844  sin0pilem1  12862  pilem3  12864  ef2kpi  12887  sin2pim  12894  cos2pim  12895  sinmpi  12896  cosmpi  12897  sinppi  12898  cosppi  12899  sinhalfpip  12901  sinhalfpim  12902  coshalfpip  12903  coshalfpim  12904  tangtx  12919  ex-ceil  12938  qdencn  13222  cvgcmp2nlemabs  13227  trilpolemlt1  13234