Theorem syl5eq 2210

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

Syntax hints:   -> wi 4   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  eqtr2id  2211  eqtr3id  2212  3eqtr3a  2222  3eqtr4g  2223  csbtt  3056  csbvarg  3072  csbie2g  3094  rabbi2dva  3329  csbprc  3453  disjssun  3471  disjpr2  3639  prprc2  3684  difprsn2  3712  opprc  3778  intsng  3857  riinm  3937  iinxsng  3938  iunxprg  3945  rintm  3957  sucprc  4389  unisucg  4391  xpriindim  4741  relop  4753  dmxpm  4823  riinint  4864  resabs1  4912  resabs2  4914  resima2  4917  xpssres  4918  resopab2  4930  imasng  4968  ndmima  4980  xpdisj1  5027  xpdisj2  5028  djudisj  5030  resdisj  5031  rnxpm  5032  xpima1  5049  xpima2m  5050  dmsnsnsng  5080  rnsnopg  5081  rnpropg  5082  mptiniseg  5097  dfco2a  5103  relcoi1  5134  unixpm  5138  iotaval  5163  funtp  5240  fnun  5293  fnresdisj  5297  fnima  5305  fnimaeq0  5308  fcoi1  5367  f1orescnv  5447  foun  5450  resdif  5453  tz6.12-2  5476  fveu  5477  tz6.12-1  5512  fvun2  5552  fvopab3ig  5559  f1oresrab  5649  dfmptg  5663  ressnop0  5665  fvunsng  5678  fnsnsplitss  5683  fsnunfv  5685  fvpr1  5688  fvpr2  5689  fvpr1g  5690  fvpr2g  5691  fvtp1g  5692  fvtp2g  5693  fvtp3g  5694  fvtp2  5696  fvtp3  5697  f1oiso2  5794  riotaund  5831  ovprc  5873  resoprab2  5935  fnoprabg  5939  ovidig  5955  ovigg  5958  ov6g  5975  ovconst2  5989  offval2  6064  ot1stg  6117  ot2ndg  6118  ot3rdgg  6119  fmpoco  6180  algrflemg  6194  tpostpos2  6229  rdgisuc1  6348  frec0g  6361  frecsuclem  6370  frecrdg  6372  oasuc  6428  oa1suc  6431  omsuc  6436  nnm1  6488  nnm2  6489  dfec2  6500  errn  6519  ixpsnval  6663  ixpintm  6687  mapen  6808  xpmapenlem  6811  phplem2  6815  undifdc  6885  fisseneq  6893  ssfirab  6895  eqinfti  6981  infvalti  6983  infsnti  6991  casef  7049  caseinl  7052  caseinr  7053  djudom  7054  ctssdccl  7072  exmidfodomrlemim  7153  1qec  7325  mulidnq  7326  addpinq1  7401  suplocexprlem2b  7651  suplocexprlemlub  7661  0idsr  7704  1idsr  7705  caucvgsrlemoffres  7737  caucvgsr  7739  mulresr  7775  pitonnlem2  7784  ax1rid  7814  axcnre  7818  negid  8141  subneg  8143  negneg  8144  dfinfre  8847  2times  8981  infrenegsupex  9528  rexneg  9762  xaddpnf2  9779  xaddmnf1  9780  xaddmnf2  9781  fseq1p1m1  10025  fzosplitprm1  10165  intfracq  10251  frec2uz0d  10330  frec2uzrdg  10340  frecuzrdg0  10344  frecuzrdgg  10347  frecuzrdg0t  10353  seq3val  10389  seqvalcd  10390  iseqf1olemjpcl  10426  iseqf1olemqpcl  10427  iseqf1olemfvp  10428  seq3f1olemqsum  10431  sqval  10509  iexpcyc  10555  binom3  10568  faclbnd  10650  faclbnd2  10651  bcn1  10667  hashinfom  10687  hashennn  10689  hashxp  10735  shftlem  10754  shftuz  10755  shftidt  10771  reim0  10799  remullem  10809  resqrexlemf1  10946  resqrexlemcalc3  10954  absexpzap  11018  absimle  11022  amgm2  11056  minmax  11167  mingeb  11179  2zinfmin  11180  xrmaxiflemval  11187  xrmaxadd  11198  infxrnegsupex  11200  xrminmax  11202  summodc  11320  fsum3  11324  sumsnf  11346  sumsns  11352  isumclim3  11360  isumge0  11367  fsump1i  11370  fsum2dlemstep  11371  fisumcom2  11375  fsumshftm  11382  fsumconst  11391  fsumiun  11414  hashrabrex  11418  hashuni  11419  binom11  11423  isumsplit  11428  geo2sum  11451  mertensabs  11474  prodmodc  11515  fprodseq  11520  prodsnf  11529  prodsns  11540  fprodconst  11557  fprod2dlemstep  11559  fprodcom2fi  11563  efgt1p2  11632  efgt1p  11633  resinval  11652  recosval  11653  cosadd  11674  ef01bndlem  11693  eirraplem  11713  ialgr0  11972  algrp1  11974  eucalg  11987  phiprmpw  12150  phiprm  12151  prmdiv  12163  pythagtriplem12  12203  pythagtriplem14  12205  pythagtriplem16  12207  pceu  12223  pcfac  12276  prmpwdvds  12281  4sqlem5  12308  mul4sqlem  12319  ennnfonelem0  12334  ennnfonelemfun  12346  ennnfonelemf1  12347  ennnfonelemrn  12348  ctinfomlemom  12356  nninfdclemp1  12379  ndxid  12414  setsfun0  12426  setsresg  12428  setscom  12430  strslfv2d  12432  ressid2  12449  ressval2  12450  tgidm  12674  tgrest  12769  ssidcn  12810  txcnmpt  12873  txcn  12875  blres  13034  mopnval  13042  remetdval  13139  divccncfap  13177  cncfmet  13179  cncfcncntop  13180  cnplimcim  13236  cnplimclemr  13238  limccnpcntop  13244  limccnp2cntop  13246  dvexp  13275  sin0pilem1  13302  pilem3  13304  ef2kpi  13327  sin2pim  13334  cos2pim  13335  sinmpi  13336  cosmpi  13337  sinppi  13338  cosppi  13339  sinhalfpip  13341  sinhalfpim  13342  coshalfpip  13343  coshalfpim  13344  tangtx  13359  1cxp  13421  ecxp  13422  rplogb1  13466  rpelogb  13467  binom4  13497  lgslem1  13501  2sqlem8  13559  ex-ceil  13567  qdencn  13866  cvgcmp2nlemabs  13871  trilpolemlt1  13880  nconstwlpolem0  13901