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 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  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  3139  csbvarg  3155  csbie2g  3178  rabbi2dva  3415  csbprc  3540  disjssun  3558  disjpr2  3733  rabsnif  3738  prprc2  3781  difprsn2  3813  opprc  3883  intsng  3962  riinm  4043  iinxsng  4044  iunxprg  4051  rintm  4063  sucprc  4509  unisucg  4511  xpriindim  4868  relop  4880  dmxpm  4952  riinint  4993  resabs1  5042  resabs2  5044  resima2  5047  xpssres  5048  resopab2  5060  mptimass  5089  imasng  5101  ndmima  5113  xpdisj1  5161  xpdisj2  5162  djudisj  5164  resdisj  5165  rnxpm  5166  xpima1  5183  xpima2m  5184  dmsnsnsng  5214  rnsnopg  5215  rnpropg  5216  mptiniseg  5231  dfco2a  5237  relcoi1  5268  unixpm  5272  iotaval  5298  funtp  5383  fnun  5438  fnresdisj  5442  fnima  5451  fnimaeq0  5454  fcoi1  5517  f1orescnv  5599  foun  5602  resdif  5605  tz6.12-2  5630  fveu  5631  tz6.12-1  5666  fvun2  5713  fvopab3ig  5720  f1oresrab  5812  dfmptg  5827  funopsn  5830  ressnop0  5835  fvunsng  5848  fnsnsplitss  5853  fsnunfv  5855  fvpr1  5858  fvpr2  5859  fvpr1g  5860  fvpr2g  5861  fvtp1g  5862  fvtp2g  5863  fvtp3g  5864  fvtp2  5866  fvtp3  5867  f1oiso2  5968  riotaund  6008  ovprc  6054  resoprab2  6118  fnoprabg  6122  ovidig  6139  ovigg  6142  fvmpopr2d  6158  ov6g  6160  ovconst2  6174  offval2  6251  ot1stg  6315  ot2ndg  6316  ot3rdgg  6317  opabn1stprc  6358  fmpoco  6381  algrflemg  6395  tpostpos2  6431  rdgisuc1  6550  frec0g  6563  frecsuclem  6572  frecrdg  6574  oasuc  6632  oa1suc  6635  omsuc  6640  nnm1  6693  nnm2  6694  dfec2  6705  errn  6724  ixpsnval  6870  ixpintm  6894  mapen  7032  xpmapenlem  7035  phplem2  7039  undifdc  7116  prfidceq  7120  fisseneq  7127  ssfirab  7129  eqinfti  7219  infvalti  7221  infsnti  7229  casef  7287  caseinl  7290  caseinr  7291  djudom  7292  ctssdccl  7310  nninfwlpoimlemginf  7375  exmidfodomrlemim  7412  1qec  7608  mulidnq  7609  addpinq1  7684  suplocexprlem2b  7934  suplocexprlemlub  7944  0idsr  7987  1idsr  7988  caucvgsrlemoffres  8020  caucvgsr  8022  mulresr  8058  pitonnlem2  8067  ax1rid  8097  axcnre  8101  negid  8426  subneg  8428  negneg  8429  dfinfre  9136  2times  9271  infrenegsupex  9828  rexneg  10065  xaddpnf2  10082  xaddmnf1  10083  xaddmnf2  10084  fseq1p1m1  10329  fzosplitprm1  10481  intfracq  10583  frec2uz0d  10662  frec2uzrdg  10672  frecuzrdg0  10676  frecuzrdgg  10679  frecuzrdg0t  10685  seq3val  10723  seqvalcd  10724  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  iseqf1olemfvp  10773  seq3f1olemqsum  10776  seqf1oglem2  10783  sqval  10860  iexpcyc  10907  binom3  10920  faclbnd  11004  faclbnd2  11005  bcn1  11021  hashinfom  11041  hashennn  11043  hashxp  11091  hashtpgim  11110  hashtpglem  11111  hashtpg  11112  csbwrdg  11147  ccatlid  11187  s1val  11198  swrd00g  11234  pfxclz  11264  pfxccatpfx2  11322  cats1fvn  11349  cats1fvd  11351  cats1lend  11352  shftlem  11394  shftuz  11395  shftidt  11411  reim0  11439  remullem  11449  resqrexlemf1  11586  resqrexlemcalc3  11594  absexpzap  11658  absimle  11662  amgm2  11696  minmax  11808  mingeb  11820  2zinfmin  11821  xrmaxiflemval  11828  xrmaxadd  11839  infxrnegsupex  11841  xrminmax  11843  summodc  11962  fsum3  11966  sumsnf  11988  sumsns  11994  isumclim3  12002  isumge0  12009  fsump1i  12012  fsum2dlemstep  12013  fisumcom2  12017  fsumshftm  12024  fsumconst  12033  fsumiun  12056  hashrabrex  12060  hashuni  12061  binom11  12065  isumsplit  12070  geo2sum  12093  mertensabs  12116  prodmodc  12157  fprodseq  12162  prodsnf  12171  prodsns  12182  fprodconst  12199  fprod2dlemstep  12201  fprodcom2fi  12205  efgt1p2  12274  efgt1p  12275  resinval  12294  recosval  12295  cosadd  12316  ef01bndlem  12335  eirraplem  12356  bits0  12527  nninfctlemfo  12629  ialgr0  12634  algrp1  12636  eucalg  12649  phiprmpw  12812  phiprm  12813  prmdiv  12825  pythagtriplem12  12866  pythagtriplem14  12868  pythagtriplem16  12870  pceu  12886  pcfac  12941  prmpwdvds  12946  4sqlem5  12973  mul4sqlem  12984  ennnfonelem0  13044  ennnfonelemfun  13056  ennnfonelemf1  13057  ennnfonelemrn  13058  ctinfomlemom  13066  nninfdclemp1  13089  ndxid  13124  setsfun0  13136  setsresg  13138  setscom  13140  strslfv2d  13143  basm  13162  ressval3d  13173  resseqnbasd  13174  prdsval  13374  pwsval  13392  pwsplusgval  13396  pwsmulrval  13397  imasaddvallemg  13416  xpsval  13453  plusffvalg  13463  mgm1  13471  grpidvalg  13474  sgrp1  13512  prdsidlem  13548  mnd1  13556  mnd1id  13557  subsubm  13584  grppropstrg  13620  grpinvfvalg  13643  grpsubfvalg  13646  grp1  13707  prdsinvlem  13709  pwsinvg  13713  mulgfvalg  13726  mulgnn0gsum  13733  mulg2  13736  subsubg  13802  releqgg  13825  eqgfval  13827  conjsubg  13882  gsumfzconstf  13947  mgpvalg  13955  mgpbasg  13958  mgpscag  13959  mgptopng  13961  mgpdsg  13962  mgpress  13963  ringidvalg  13993  ring1  14091  opprvalg  14101  opprmulfvalg  14102  opprbasg  14107  oppraddg  14108  subsubrng  14247  subsubrg  14278  rrgval  14295  scaffvalg  14339  lmodpropd  14382  lsssetm  14389  lsslss  14414  lspfval  14421  sraring  14482  lidlvalg  14504  rspvalg  14505  lidlss  14509  islidlm  14512  lidl0cl  14516  lidlacl  14517  lidlnegcl  14518  lidl0  14522  lidl1  14523  rspcl  14524  rspssid  14525  rsp0  14526  rspssp  14527  2idlval  14535  2idlvalg  14536  crngridl  14563  rspsn  14567  zrhval  14650  zrhvalg  14651  zlmval  14660  zlmbasg  14662  zlmplusgg  14663  zlmmulrg  14664  znval  14669  znzrh2  14679  znf1o  14684  psrval  14699  mplvalcoe  14723  mpl0fi  14735  mplnegfi  14738  tgidm  14817  tgrest  14912  ssidcn  14953  txcnmpt  15016  txcn  15018  blres  15177  mopnval  15185  remetdval  15290  expcn  15312  divccncfap  15333  cncfmet  15335  cncfcncntop  15336  hovergt0  15393  cnplimcim  15410  cnplimclemr  15412  limccnpcntop  15418  limccnp2cntop  15420  dvexp  15454  dvmptid  15459  dvmptfsum  15468  elply2  15478  elplyd  15484  plyaddlem1  15490  plymullem1  15491  plycjlemc  15503  sin0pilem1  15524  pilem3  15526  ef2kpi  15549  sin2pim  15556  cos2pim  15557  sinmpi  15558  cosmpi  15559  sinppi  15560  cosppi  15561  sinhalfpip  15563  sinhalfpim  15564  coshalfpip  15565  coshalfpim  15566  tangtx  15581  1cxp  15643  ecxp  15644  rplogb1  15691  rpelogb  15692  binom4  15722  0sgm  15728  fsumdvdsmul  15734  1sgmprm  15737  1sgm2ppw  15738  lgslem1  15748  gausslemma2dlem4  15812  lgseisenlem1  15818  lgseisenlem2  15819  lgseisenlem3  15820  lgseisenlem4  15821  lgseisen  15822  lgsquadlem1  15825  lgsquadlem2  15826  lgsquadlem3  15827  lgsquad2lem1  15829  m1lgs  15833  2lgslem3a  15841  2lgslem3b  15842  2lgslem3c  15843  2lgslem3d  15844  2sqlem8  15871  opvtxov  15893  opiedgov  15896  structiedg0val  15910  edgov  15933  edg0iedg0g  15936  upgredg  16014  usgrf1oedg  16075  ushgredgedg  16096  ushgredgedgloop  16098  griedg0ssusgr  16121  subgrprop3  16132  0uhgrsubgr  16135  vtxdgfval  16158  vtxdfifiun  16167  vtxdumgrfival  16168  vtxd0nedgbfi  16169  1hevtxdg1en  16178  upgriswlkdc  16230  wlkres  16249  trlreslem  16259  clwwlkn2  16291  eupthvdres  16345  eupth2lem3fi  16346  ex-ceil  16369  depindlem1  16376  qdencn  16682  cvgcmp2nlemabs  16687  trilpolemlt1  16696  nconstwlpolem0  16719  gfsump1  16738  gfsumcl  16739