Theorem eqtrid 2250

Description: An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem eqtrid

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

Syntax hints:   -> wi 4   = wceq 1373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198

This theorem is referenced by:  eqtr2id  2251  eqtr3id  2252  3eqtr3a  2262  3eqtr4g  2263  csbtt  3105  csbvarg  3121  csbie2g  3144  rabbi2dva  3381  csbprc  3506  disjssun  3524  disjpr2  3697  prprc2  3742  difprsn2  3773  opprc  3840  intsng  3919  riinm  4000  iinxsng  4001  iunxprg  4008  rintm  4020  sucprc  4459  unisucg  4461  xpriindim  4816  relop  4828  dmxpm  4898  riinint  4939  resabs1  4988  resabs2  4990  resima2  4993  xpssres  4994  resopab2  5006  mptimass  5035  imasng  5047  ndmima  5059  xpdisj1  5107  xpdisj2  5108  djudisj  5110  resdisj  5111  rnxpm  5112  xpima1  5129  xpima2m  5130  dmsnsnsng  5160  rnsnopg  5161  rnpropg  5162  mptiniseg  5177  dfco2a  5183  relcoi1  5214  unixpm  5218  iotaval  5243  funtp  5327  fnun  5382  fnresdisj  5386  fnima  5394  fnimaeq0  5397  fcoi1  5456  f1orescnv  5538  foun  5541  resdif  5544  tz6.12-2  5567  fveu  5568  tz6.12-1  5603  fvun2  5646  fvopab3ig  5653  f1oresrab  5745  dfmptg  5759  funopsn  5762  ressnop0  5765  fvunsng  5778  fnsnsplitss  5783  fsnunfv  5785  fvpr1  5788  fvpr2  5789  fvpr1g  5790  fvpr2g  5791  fvtp1g  5792  fvtp2g  5793  fvtp3g  5794  fvtp2  5796  fvtp3  5797  f1oiso2  5896  riotaund  5934  ovprc  5980  resoprab2  6042  fnoprabg  6046  ovidig  6063  ovigg  6066  fvmpopr2d  6082  ov6g  6084  ovconst2  6098  offval2  6174  ot1stg  6238  ot2ndg  6239  ot3rdgg  6240  fmpoco  6302  algrflemg  6316  tpostpos2  6351  rdgisuc1  6470  frec0g  6483  frecsuclem  6492  frecrdg  6494  oasuc  6550  oa1suc  6553  omsuc  6558  nnm1  6611  nnm2  6612  dfec2  6623  errn  6642  ixpsnval  6788  ixpintm  6812  mapen  6943  xpmapenlem  6946  phplem2  6950  undifdc  7021  prfidceq  7025  fisseneq  7031  ssfirab  7033  eqinfti  7122  infvalti  7124  infsnti  7132  casef  7190  caseinl  7193  caseinr  7194  djudom  7195  ctssdccl  7213  nninfwlpoimlemginf  7278  exmidfodomrlemim  7309  1qec  7501  mulidnq  7502  addpinq1  7577  suplocexprlem2b  7827  suplocexprlemlub  7837  0idsr  7880  1idsr  7881  caucvgsrlemoffres  7913  caucvgsr  7915  mulresr  7951  pitonnlem2  7960  ax1rid  7990  axcnre  7994  negid  8319  subneg  8321  negneg  8322  dfinfre  9029  2times  9164  infrenegsupex  9715  rexneg  9952  xaddpnf2  9969  xaddmnf1  9970  xaddmnf2  9971  fseq1p1m1  10216  fzosplitprm1  10363  intfracq  10465  frec2uz0d  10544  frec2uzrdg  10554  frecuzrdg0  10558  frecuzrdgg  10561  frecuzrdg0t  10567  seq3val  10605  seqvalcd  10606  iseqf1olemjpcl  10653  iseqf1olemqpcl  10654  iseqf1olemfvp  10655  seq3f1olemqsum  10658  seqf1oglem2  10665  sqval  10742  iexpcyc  10789  binom3  10802  faclbnd  10886  faclbnd2  10887  bcn1  10903  hashinfom  10923  hashennn  10925  hashxp  10971  csbwrdg  11023  ccatlid  11062  s1val  11071  swrd00g  11102  shftlem  11127  shftuz  11128  shftidt  11144  reim0  11172  remullem  11182  resqrexlemf1  11319  resqrexlemcalc3  11327  absexpzap  11391  absimle  11395  amgm2  11429  minmax  11541  mingeb  11553  2zinfmin  11554  xrmaxiflemval  11561  xrmaxadd  11572  infxrnegsupex  11574  xrminmax  11576  summodc  11694  fsum3  11698  sumsnf  11720  sumsns  11726  isumclim3  11734  isumge0  11741  fsump1i  11744  fsum2dlemstep  11745  fisumcom2  11749  fsumshftm  11756  fsumconst  11765  fsumiun  11788  hashrabrex  11792  hashuni  11793  binom11  11797  isumsplit  11802  geo2sum  11825  mertensabs  11848  prodmodc  11889  fprodseq  11894  prodsnf  11903  prodsns  11914  fprodconst  11931  fprod2dlemstep  11933  fprodcom2fi  11937  efgt1p2  12006  efgt1p  12007  resinval  12026  recosval  12027  cosadd  12048  ef01bndlem  12067  eirraplem  12088  bits0  12259  nninfctlemfo  12361  ialgr0  12366  algrp1  12368  eucalg  12381  phiprmpw  12544  phiprm  12545  prmdiv  12557  pythagtriplem12  12598  pythagtriplem14  12600  pythagtriplem16  12602  pceu  12618  pcfac  12673  prmpwdvds  12678  4sqlem5  12705  mul4sqlem  12716  ennnfonelem0  12776  ennnfonelemfun  12788  ennnfonelemf1  12789  ennnfonelemrn  12790  ctinfomlemom  12798  nninfdclemp1  12821  ndxid  12856  setsfun0  12868  setsresg  12870  setscom  12872  strslfv2d  12875  basm  12893  ressval3d  12904  resseqnbasd  12905  prdsval  13105  pwsval  13123  pwsplusgval  13127  pwsmulrval  13128  imasaddvallemg  13147  xpsval  13184  plusffvalg  13194  mgm1  13202  grpidvalg  13205  sgrp1  13243  prdsidlem  13279  mnd1  13287  mnd1id  13288  subsubm  13315  grppropstrg  13351  grpinvfvalg  13374  grpsubfvalg  13377  grp1  13438  prdsinvlem  13440  pwsinvg  13444  mulgfvalg  13457  mulgnn0gsum  13464  mulg2  13467  subsubg  13533  releqgg  13556  eqgfval  13558  conjsubg  13613  gsumfzconstf  13678  mgpvalg  13685  mgpbasg  13688  mgpscag  13689  mgptopng  13691  mgpdsg  13692  mgpress  13693  ringidvalg  13723  ring1  13821  opprvalg  13831  opprmulfvalg  13832  opprbasg  13837  oppraddg  13838  subsubrng  13976  subsubrg  14007  rrgval  14024  scaffvalg  14068  lmodpropd  14111  lsssetm  14118  lsslss  14143  lspfval  14150  sraring  14211  lidlvalg  14233  rspvalg  14234  lidlss  14238  islidlm  14241  lidl0cl  14245  lidlacl  14246  lidlnegcl  14247  lidl0  14251  lidl1  14252  rspcl  14253  rspssid  14254  rsp0  14255  rspssp  14256  2idlval  14264  2idlvalg  14265  crngridl  14292  rspsn  14296  zrhval  14379  zrhvalg  14380  zlmval  14389  zlmbasg  14391  zlmplusgg  14392  zlmmulrg  14393  znval  14398  znzrh2  14408  znf1o  14413  psrval  14428  mplvalcoe  14452  mpl0fi  14464  mplnegfi  14467  tgidm  14546  tgrest  14641  ssidcn  14682  txcnmpt  14745  txcn  14747  blres  14906  mopnval  14914  remetdval  15019  expcn  15041  divccncfap  15062  cncfmet  15064  cncfcncntop  15065  hovergt0  15122  cnplimcim  15139  cnplimclemr  15141  limccnpcntop  15147  limccnp2cntop  15149  dvexp  15183  dvmptid  15188  dvmptfsum  15197  elply2  15207  elplyd  15213  plyaddlem1  15219  plymullem1  15220  plycjlemc  15232  sin0pilem1  15253  pilem3  15255  ef2kpi  15278  sin2pim  15285  cos2pim  15286  sinmpi  15287  cosmpi  15288  sinppi  15289  cosppi  15290  sinhalfpip  15292  sinhalfpim  15293  coshalfpip  15294  coshalfpim  15295  tangtx  15310  1cxp  15372  ecxp  15373  rplogb1  15420  rpelogb  15421  binom4  15451  0sgm  15457  fsumdvdsmul  15463  1sgmprm  15466  1sgm2ppw  15467  lgslem1  15477  gausslemma2dlem4  15541  lgseisenlem1  15547  lgseisenlem2  15548  lgseisenlem3  15549  lgseisenlem4  15550  lgseisen  15551  lgsquadlem1  15554  lgsquadlem2  15555  lgsquadlem3  15556  lgsquad2lem1  15558  m1lgs  15562  2lgslem3a  15570  2lgslem3b  15571  2lgslem3c  15572  2lgslem3d  15573  2sqlem8  15600  opvtxov  15620  opiedgov  15623  structiedg0val  15637  edgov  15655  ex-ceil  15662  qdencn  15966  cvgcmp2nlemabs  15971  trilpolemlt1  15980  nconstwlpolem0  16002