Theorem eqtrid 2276

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

Syntax hints:   -> wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  eqtr2id  2277  eqtr3id  2278  3eqtr3a  2288  3eqtr4g  2289  csbtt  3140  csbvarg  3156  csbie2g  3179  rabbi2dva  3417  csbprc  3542  disjssun  3560  disjpr2  3737  rabsnif  3742  prprc2  3785  difprsn2  3818  opprc  3888  intsng  3967  riinm  4048  iinxsng  4049  iunxprg  4056  rintm  4068  sucprc  4515  unisucg  4517  xpriindim  4874  relop  4886  dmxpm  4958  riinint  4999  resabs1  5048  resabs2  5050  resima2  5053  xpssres  5054  resopab2  5066  mptimass  5095  imasng  5108  ndmima  5120  xpdisj1  5168  xpdisj2  5169  djudisj  5171  resdisj  5172  rnxpm  5173  xpima1  5190  xpima2m  5191  dmsnsnsng  5221  rnsnopg  5222  rnpropg  5223  mptiniseg  5238  dfco2a  5244  relcoi1  5275  unixpm  5279  iotaval  5305  funtp  5390  fnun  5445  fnresdisj  5449  fnima  5458  fnimaeq0  5461  fcoi1  5525  f1orescnv  5608  foun  5611  resdif  5614  tz6.12-2  5639  fveu  5640  tz6.12-1  5675  fvun2  5722  fvopab3ig  5729  f1oresrab  5820  dfmptg  5835  funopsn  5838  ressnop0  5843  fvunsng  5856  fnsnsplitss  5861  fsnunfv  5863  fvpr1  5866  fvpr2  5867  fvpr1g  5868  fvpr2g  5869  fvtp1g  5870  fvtp2g  5871  fvtp3g  5872  fvtp2  5874  fvtp3  5875  f1oiso2  5978  riotaund  6018  ovprc  6064  resoprab2  6128  fnoprabg  6132  ovidig  6149  ovigg  6152  fvmpopr2d  6168  ov6g  6170  ovconst2  6184  offval2  6260  ot1stg  6324  ot2ndg  6325  ot3rdgg  6326  opabn1stprc  6367  fmpoco  6390  algrflemg  6404  suppsnopdc  6428  tpostpos2  6474  rdgisuc1  6593  frec0g  6606  frecsuclem  6615  frecrdg  6617  oasuc  6675  oa1suc  6678  omsuc  6683  nnm1  6736  nnm2  6737  dfec2  6748  errn  6767  ixpsnval  6913  ixpintm  6937  mapen  7075  xpmapenlem  7078  phplem2  7082  undifdc  7159  prfidceq  7163  fisseneq  7170  ssfirab  7172  eqinfti  7279  infvalti  7281  infsnti  7289  casef  7347  caseinl  7350  caseinr  7351  djudom  7352  ctssdccl  7370  nninfwlpoimlemginf  7435  exmidfodomrlemim  7472  1qec  7668  mulidnq  7669  addpinq1  7744  suplocexprlem2b  7994  suplocexprlemlub  8004  0idsr  8047  1idsr  8048  caucvgsrlemoffres  8080  caucvgsr  8082  mulresr  8118  pitonnlem2  8127  ax1rid  8157  axcnre  8161  negid  8485  subneg  8487  negneg  8488  dfinfre  9195  2times  9330  infrenegsupex  9889  rexneg  10126  xaddpnf2  10143  xaddmnf1  10144  xaddmnf2  10145  fseq1p1m1  10391  fzosplitprm1  10543  intfracq  10645  frec2uz0d  10724  frec2uzrdg  10734  frecuzrdg0  10738  frecuzrdgg  10741  frecuzrdg0t  10747  seq3val  10785  seqvalcd  10786  iseqf1olemjpcl  10833  iseqf1olemqpcl  10834  iseqf1olemfvp  10835  seq3f1olemqsum  10838  seqf1oglem2  10845  sqval  10922  iexpcyc  10969  binom3  10982  faclbnd  11066  faclbnd2  11067  bcn1  11083  hashinfom  11103  hashennn  11105  hashxp  11153  hashtpgim  11172  hashtpglem  11173  hashtpg  11174  csbwrdg  11209  ccatlid  11249  s1val  11260  swrd00g  11296  pfxclz  11326  pfxccatpfx2  11384  cats1fvn  11411  cats1fvd  11413  cats1lend  11414  shftlem  11456  shftuz  11457  shftidt  11473  reim0  11501  remullem  11511  resqrexlemf1  11648  resqrexlemcalc3  11656  absexpzap  11720  absimle  11724  amgm2  11758  minmax  11870  mingeb  11882  2zinfmin  11883  xrmaxiflemval  11890  xrmaxadd  11901  infxrnegsupex  11903  xrminmax  11905  summodc  12024  fsum3  12028  sumsnf  12050  sumsns  12056  isumclim3  12064  isumge0  12071  fsump1i  12074  fsum2dlemstep  12075  fisumcom2  12079  fsumshftm  12086  fsumconst  12095  fsumiun  12118  hashrabrex  12122  hashuni  12123  binom11  12127  isumsplit  12132  geo2sum  12155  mertensabs  12178  prodmodc  12219  fprodseq  12224  prodsnf  12233  prodsns  12244  fprodconst  12261  fprod2dlemstep  12263  fprodcom2fi  12267  efgt1p2  12336  efgt1p  12337  resinval  12356  recosval  12357  cosadd  12378  ef01bndlem  12397  eirraplem  12418  bits0  12589  nninfctlemfo  12691  ialgr0  12696  algrp1  12698  eucalg  12711  phiprmpw  12874  phiprm  12875  prmdiv  12887  pythagtriplem12  12928  pythagtriplem14  12930  pythagtriplem16  12932  pceu  12948  pcfac  13003  prmpwdvds  13008  4sqlem5  13035  mul4sqlem  13046  ennnfonelem0  13106  ennnfonelemfun  13118  ennnfonelemf1  13119  ennnfonelemrn  13120  ctinfomlemom  13128  nninfdclemp1  13151  ndxid  13186  setsfun0  13198  setsresg  13200  setscom  13202  strslfv2d  13205  basm  13224  ressval3d  13235  resseqnbasd  13236  prdsval  13436  pwsval  13454  pwsplusgval  13458  pwsmulrval  13459  imasaddvallemg  13478  xpsval  13515  plusffvalg  13525  mgm1  13533  grpidvalg  13536  sgrp1  13574  prdsidlem  13610  mnd1  13618  mnd1id  13619  subsubm  13646  grppropstrg  13682  grpinvfvalg  13705  grpsubfvalg  13708  grp1  13769  prdsinvlem  13771  pwsinvg  13775  mulgfvalg  13788  mulgnn0gsum  13795  mulg2  13798  subsubg  13864  releqgg  13887  eqgfval  13889  conjsubg  13944  gsumfzconstf  14009  mgpvalg  14017  mgpbasg  14020  mgpscag  14021  mgptopng  14023  mgpdsg  14024  mgpress  14025  ringidvalg  14055  ring1  14153  opprvalg  14163  opprmulfvalg  14164  opprbasg  14169  oppraddg  14170  subsubrng  14309  subsubrg  14340  rrgval  14357  scaffvalg  14402  lmodpropd  14445  lsssetm  14452  lsslss  14477  lspfval  14484  sraring  14545  lidlvalg  14567  rspvalg  14568  lidlss  14572  islidlm  14575  lidl0cl  14579  lidlacl  14580  lidlnegcl  14581  lidl0  14585  lidl1  14586  rspcl  14587  rspssid  14588  rsp0  14589  rspssp  14590  2idlval  14598  2idlvalg  14599  crngridl  14626  rspsn  14630  zrhval  14713  zrhvalg  14714  zlmval  14723  zlmbasg  14725  zlmplusgg  14726  zlmmulrg  14727  znval  14732  znzrh2  14742  znf1o  14747  psrval  14762  mplvalcoe  14791  mpl0fi  14803  mplnegfi  14806  tgidm  14885  tgrest  14980  ssidcn  15021  txcnmpt  15084  txcn  15086  blres  15245  mopnval  15253  remetdval  15358  expcn  15380  divccncfap  15401  cncfmet  15403  cncfcncntop  15404  hovergt0  15461  cnplimcim  15478  cnplimclemr  15480  limccnpcntop  15486  limccnp2cntop  15488  dvexp  15522  dvmptid  15527  dvmptfsum  15536  elply2  15546  elplyd  15552  plyaddlem1  15558  plymullem1  15559  plycjlemc  15571  sin0pilem1  15592  pilem3  15594  ef2kpi  15617  sin2pim  15624  cos2pim  15625  sinmpi  15626  cosmpi  15627  sinppi  15628  cosppi  15629  sinhalfpip  15631  sinhalfpim  15632  coshalfpip  15633  coshalfpim  15634  tangtx  15649  1cxp  15711  ecxp  15712  rplogb1  15759  rpelogb  15760  binom4  15790  0sgm  15799  fsumdvdsmul  15805  1sgmprm  15808  1sgm2ppw  15809  lgslem1  15819  gausslemma2dlem4  15883  lgseisenlem1  15889  lgseisenlem2  15890  lgseisenlem3  15891  lgseisenlem4  15892  lgseisen  15893  lgsquadlem1  15896  lgsquadlem2  15897  lgsquadlem3  15898  lgsquad2lem1  15900  m1lgs  15904  2lgslem3a  15912  2lgslem3b  15913  2lgslem3c  15914  2lgslem3d  15915  2sqlem8  15942  opvtxov  15964  opiedgov  15967  structiedg0val  15981  edgov  16004  edg0iedg0g  16007  upgredg  16085  usgrf1oedg  16146  ushgredgedg  16167  ushgredgedgloop  16169  griedg0ssusgr  16192  subgrprop3  16203  0uhgrsubgr  16206  vtxdgfval  16229  vtxdfifiun  16238  vtxdumgrfival  16239  vtxd0nedgbfi  16240  1hevtxdg1en  16249  upgriswlkdc  16301  wlkres  16320  trlreslem  16330  clwwlkn2  16362  eupthvdres  16416  eupth2lem3fi  16417  ex-ceil  16440  depindlem1  16447  qdencn  16755  cvgcmp2nlemabs  16764  trilpolemlt1  16773  nconstwlpolem0  16796  gfsump1  16815  gfsumcl  16816