Theorem syl5eq 2185

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 2173	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1332

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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

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

This theorem is referenced by:  syl5req  2186  syl5eqr  2187  3eqtr3a  2197  3eqtr4g  2198  csbtt  3019  csbvarg  3035  csbie2g  3055  rabbi2dva  3289  csbprc  3413  disjssun  3431  disjpr2  3595  prprc2  3640  difprsn2  3668  opprc  3734  intsng  3813  riinm  3893  iinxsng  3894  iunxprg  3901  rintm  3913  sucprc  4342  unisucg  4344  xpriindim  4685  relop  4697  dmxpm  4767  riinint  4808  resabs1  4856  resabs2  4858  resima2  4861  xpssres  4862  resopab2  4874  imasng  4912  ndmima  4924  xpdisj1  4971  xpdisj2  4972  djudisj  4974  resdisj  4975  rnxpm  4976  xpima1  4993  xpima2m  4994  dmsnsnsng  5024  rnsnopg  5025  rnpropg  5026  mptiniseg  5041  dfco2a  5047  relcoi1  5078  unixpm  5082  iotaval  5107  funtp  5184  fnun  5237  fnresdisj  5241  fnima  5249  fnimaeq0  5252  fcoi1  5311  f1orescnv  5391  foun  5394  resdif  5397  tz6.12-2  5420  fveu  5421  tz6.12-1  5456  fvun2  5496  fvopab3ig  5503  f1oresrab  5593  dfmptg  5607  ressnop0  5609  fvunsng  5622  fnsnsplitss  5627  fsnunfv  5629  fvpr1  5632  fvpr2  5633  fvpr1g  5634  fvpr2g  5635  fvtp1g  5636  fvtp2g  5637  fvtp3g  5638  fvtp2  5640  fvtp3  5641  f1oiso2  5736  riotaund  5772  ovprc  5814  resoprab2  5876  fnoprabg  5880  ovidig  5896  ovigg  5899  ov6g  5916  ovconst2  5930  offval2  6005  ot1stg  6058  ot2ndg  6059  ot3rdgg  6060  fmpoco  6121  algrflemg  6135  tpostpos2  6170  rdgisuc1  6289  frec0g  6302  frecsuclem  6311  frecrdg  6313  oasuc  6368  oa1suc  6371  omsuc  6376  nnm1  6428  nnm2  6429  dfec2  6440  errn  6459  ixpsnval  6603  ixpintm  6627  mapen  6748  xpmapenlem  6751  phplem2  6755  undifdc  6820  fisseneq  6828  ssfirab  6830  eqinfti  6915  infvalti  6917  infsnti  6925  casef  6981  caseinl  6984  caseinr  6985  djudom  6986  ctssdccl  7004  exmidfodomrlemim  7074  1qec  7220  mulidnq  7221  addpinq1  7296  suplocexprlem2b  7546  suplocexprlemlub  7556  0idsr  7599  1idsr  7600  caucvgsrlemoffres  7632  caucvgsr  7634  mulresr  7670  pitonnlem2  7679  ax1rid  7709  axcnre  7713  negid  8033  subneg  8035  negneg  8036  dfinfre  8738  2times  8872  infrenegsupex  9416  rexneg  9643  xaddpnf2  9660  xaddmnf1  9661  xaddmnf2  9662  fseq1p1m1  9905  fzosplitprm1  10042  intfracq  10124  frec2uz0d  10203  frec2uzrdg  10213  frecuzrdg0  10217  frecuzrdgg  10220  frecuzrdg0t  10226  seq3val  10262  seqvalcd  10263  iseqf1olemjpcl  10299  iseqf1olemqpcl  10300  iseqf1olemfvp  10301  seq3f1olemqsum  10304  sqval  10382  iexpcyc  10428  binom3  10440  faclbnd  10519  faclbnd2  10520  bcn1  10536  hashinfom  10556  hashennn  10558  hashxp  10604  shftlem  10620  shftuz  10621  shftidt  10637  reim0  10665  remullem  10675  resqrexlemf1  10812  resqrexlemcalc3  10820  absexpzap  10884  absimle  10888  amgm2  10922  minmax  11033  xrmaxiflemval  11051  xrmaxadd  11062  infxrnegsupex  11064  xrminmax  11066  summodc  11184  fsum3  11188  sumsnf  11210  sumsns  11216  isumclim3  11224  isumge0  11231  fsump1i  11234  fsum2dlemstep  11235  fisumcom2  11239  fsumshftm  11246  fsumconst  11255  fsumiun  11278  hashrabrex  11282  hashuni  11283  binom11  11287  isumsplit  11292  geo2sum  11315  mertensabs  11338  prodmodc  11379  fprodseq  11384  efgt1p2  11438  efgt1p  11439  resinval  11458  recosval  11459  cosadd  11480  ef01bndlem  11499  eirraplem  11519  ialgr0  11761  algrp1  11763  eucalg  11776  phiprmpw  11934  phiprm  11935  ennnfonelem0  11954  ennnfonelemfun  11966  ennnfonelemf1  11967  ennnfonelemrn  11968  ctinfomlemom  11976  ndxid  12022  setsfun0  12034  setsresg  12036  setscom  12038  strslfv2d  12040  ressid2  12057  ressval2  12058  tgidm  12282  tgrest  12377  ssidcn  12418  txcnmpt  12481  txcn  12483  blres  12642  mopnval  12650  remetdval  12747  divccncfap  12785  cncfmet  12787  cncfcncntop  12788  cnplimcim  12844  cnplimclemr  12846  limccnpcntop  12852  limccnp2cntop  12854  dvexp  12883  sin0pilem1  12910  pilem3  12912  ef2kpi  12935  sin2pim  12942  cos2pim  12943  sinmpi  12944  cosmpi  12945  sinppi  12946  cosppi  12947  sinhalfpip  12949  sinhalfpim  12950  coshalfpip  12951  coshalfpim  12952  tangtx  12967  1cxp  13029  ecxp  13030  rplogb1  13073  rpelogb  13074  ex-ceil  13109  qdencn  13397  cvgcmp2nlemabs  13402  trilpolemlt1  13409