Theorem eqtrid 2277

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 2265	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 2214

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

This theorem is referenced by:  eqtr2id  2278  eqtr3id  2279  3eqtr3a  2289  3eqtr4g  2290  eqab  2367  csbtt  3150  csbvarg  3166  csbie2g  3189  rabbi2dva  3429  csbprc  3554  disjssun  3572  disjpr2  3753  rabsnif  3758  prprc2  3801  difprsn2  3834  opprc  3904  intsng  3983  riinm  4064  iinxsng  4065  iunxprg  4072  rintm  4084  sucprc  4533  unisucg  4535  xpriindim  4893  relop  4905  dmxpm  4977  riinint  5018  resabs1  5067  resabs2  5069  resima2  5072  xpssres  5073  resopab2  5085  mptimass  5114  imasng  5127  ndmima  5139  xpdisj1  5187  xpdisj2  5188  djudisj  5190  resdisj  5191  rnxpm  5192  xpima1  5209  xpima2m  5210  dmsnsnsng  5240  rnsnopg  5241  rnpropg  5242  mptiniseg  5257  dfco2a  5263  relcoi1  5294  unixpm  5298  iotaval  5324  funtp  5409  fnun  5464  fnresdisj  5468  fnima  5477  fnimaeq0  5480  fresaunres2disj  5545  fcoi1  5547  f1orescnv  5630  foun  5633  resdif  5636  tz6.12-2  5661  fveu  5662  tz6.12-1  5697  fvun2  5744  fvopab3ig  5751  f1oresrab  5842  dfmptg  5857  funopsn  5860  ressnop0  5865  fvunsng  5878  fnsnsplitss  5883  fsnunfv  5885  fvpr1  5888  fvpr2  5889  fvpr1g  5890  fvpr2g  5891  fvtp1g  5892  fvtp2g  5893  fvtp3g  5894  fvtp2  5896  fvtp3  5897  f1oiso2  6000  riotaund  6040  ovprc  6086  resoprab2  6150  fnoprabg  6154  ovidig  6171  ovigg  6174  fvmpopr2d  6190  ov6g  6192  ovconst2  6206  offval2  6282  ot1stg  6346  ot2ndg  6347  ot3rdgg  6348  opabn1stprc  6389  fmpoco  6412  algrflemg  6426  suppsnopdc  6450  tpostpos2  6496  rdgisuc1  6615  frec0g  6628  frecsuclem  6637  frecrdg  6639  oasuc  6697  oa1suc  6700  omsuc  6705  nnm1  6758  nnm2  6759  dfec2  6770  errn  6789  ixpsnval  6936  ixpintm  6960  mapen  7099  xpmapenlem  7102  phplem2  7107  undifdc  7184  prfidceq  7188  fisseneq  7195  ssfirab  7197  eqinfti  7311  infvalti  7313  infsnti  7321  casef  7379  caseinl  7382  caseinr  7383  djudom  7384  ctssdccl  7402  nninfwlpoimlemginf  7467  exmidfodomrlemim  7504  1qec  7703  mulidnq  7704  addpinq1  7779  suplocexprlem2b  8029  suplocexprlemlub  8039  0idsr  8082  1idsr  8083  caucvgsrlemoffres  8115  caucvgsr  8117  mulresr  8153  pitonnlem2  8162  ax1rid  8192  axcnre  8196  negid  8520  subneg  8522  negneg  8523  dfinfre  9230  2times  9365  infrenegsupex  9926  rexneg  10163  xaddpnf2  10180  xaddmnf1  10181  xaddmnf2  10182  fseq1p1m1  10428  fzosplitprm1  10580  intfracq  10682  frec2uz0d  10761  frec2uzrdg  10771  frecuzrdg0  10775  frecuzrdgg  10778  frecuzrdg0t  10784  seq3val  10822  seqvalcd  10823  iseqf1olemjpcl  10870  iseqf1olemqpcl  10871  iseqf1olemfvp  10872  seq3f1olemqsum  10875  seqf1oglem2  10882  sqval  10959  iexpcyc  11006  binom3  11019  faclbnd  11103  faclbnd2  11104  bcn1  11120  hashinfom  11141  hashennn  11143  hashxp  11191  hashfibclem  11206  hashfibc  11207  hashtpgim  11217  hashtpglem  11218  hashtpg  11219  csbwrdg  11254  ccatlid  11294  s1val  11305  swrd00g  11341  pfxclz  11371  pfxccatpfx2  11429  cats1fvn  11456  cats1fvd  11458  cats1lend  11459  shftlem  11501  shftuz  11502  shftidt  11518  reim0  11546  remullem  11556  resqrexlemf1  11693  resqrexlemcalc3  11701  absexpzap  11765  absimle  11769  amgm2  11803  minmax  11915  mingeb  11927  2zinfmin  11928  xrmaxiflemval  11935  xrmaxadd  11946  infxrnegsupex  11948  xrminmax  11950  summodc  12069  fsum3  12073  sumsnf  12095  sumsns  12101  isumclim3  12109  isumge0  12116  fsump1i  12119  fsum2dlemstep  12120  fisumcom2  12124  fsumshftm  12131  fsumconst  12140  fsumiun  12163  hashrabrex  12167  hashuni  12168  binom11  12172  isumsplit  12177  geo2sum  12200  mertensabs  12223  prodmodc  12264  fprodseq  12269  prodsnf  12278  prodsns  12289  fprodconst  12306  fprod2dlemstep  12308  fprodcom2fi  12312  efgt1p2  12381  efgt1p  12382  resinval  12401  recosval  12402  cosadd  12423  ef01bndlem  12442  eirraplem  12463  bits0  12634  nninfctlemfo  12736  ialgr0  12741  algrp1  12743  eucalg  12756  phiprmpw  12919  phiprm  12920  prmdiv  12932  pythagtriplem12  12973  pythagtriplem14  12975  pythagtriplem16  12977  pceu  12993  pcfac  13048  prmpwdvds  13053  4sqlem5  13080  mul4sqlem  13091  ennnfonelem0  13156  ennnfonelemfun  13168  ennnfonelemf1  13169  ennnfonelemrn  13170  ctinfomlemom  13178  nninfdclemp1  13201  ndxid  13236  setsfun0  13248  setsresg  13250  setscom  13252  strslfv2d  13255  basm  13274  ressval3d  13285  resseqnbasd  13286  prdsval  13486  pwsval  13504  pwsplusgval  13508  pwsmulrval  13509  imasaddvallemg  13528  xpsval  13565  plusffvalg  13575  mgm1  13583  grpidvalg  13586  sgrp1  13624  prdsidlem  13660  mnd1  13668  mnd1id  13669  subsubm  13696  grppropstrg  13732  grpinvfvalg  13755  grpsubfvalg  13758  grp1  13819  prdsinvlem  13821  pwsinvg  13825  mulgfvalg  13838  mulgnn0gsum  13845  mulg2  13848  subsubg  13914  releqgg  13937  eqgfval  13939  conjsubg  13994  gsumfzconstf  14059  mgpvalg  14067  mgpbasg  14070  mgpscag  14071  mgptopng  14073  mgpdsg  14074  mgpress  14075  ringidvalg  14105  ring1  14203  opprvalg  14213  opprmulfvalg  14214  opprbasg  14219  oppraddg  14220  subsubrng  14359  subsubrg  14390  rrgval  14407  scaffvalg  14454  lmodpropd  14497  lsssetm  14504  lsslss  14529  lspfval  14536  sraring  14597  lidlvalg  14619  rspvalg  14620  lidlss  14624  islidlm  14627  lidl0cl  14631  lidlacl  14632  lidlnegcl  14633  lidl0  14637  lidl1  14638  rspcl  14639  rspssid  14640  rsp0  14641  rspssp  14642  2idlval  14650  2idlvalg  14651  crngridl  14678  rspsn  14682  zrhval  14765  zrhvalg  14766  zlmval  14775  zlmbasg  14777  zlmplusgg  14778  zlmmulrg  14779  znval  14784  znzrh2  14794  znf1o  14799  psrval  14814  mplvalcoe  14845  mpl0fi  14857  mplnegfi  14860  tgidm  14939  tgrest  15034  ssidcn  15075  txcnmpt  15138  txcn  15140  blres  15299  mopnval  15307  remetdval  15412  expcn  15434  divccncfap  15455  cncfmet  15457  cncfcncntop  15458  hovergt0  15515  cnplimcim  15532  cnplimclemr  15534  limccnpcntop  15540  limccnp2cntop  15542  dvexp  15576  dvmptid  15581  dvmptfsum  15590  elply2  15600  elplyd  15606  plyaddlem1  15612  plymullem1  15613  plycjlemc  15625  sin0pilem1  15646  pilem3  15648  ef2kpi  15671  sin2pim  15678  cos2pim  15679  sinmpi  15680  cosmpi  15681  sinppi  15682  cosppi  15683  sinhalfpip  15685  sinhalfpim  15686  coshalfpip  15687  coshalfpim  15688  tangtx  15703  1cxp  15765  ecxp  15766  rplogb1  15813  rpelogb  15814  binom4  15844  0sgm  15853  fsumdvdsmul  15859  1sgmprm  15862  1sgm2ppw  15863  lgslem1  15873  gausslemma2dlem4  15937  lgseisenlem1  15943  lgseisenlem2  15944  lgseisenlem3  15945  lgseisenlem4  15946  lgseisen  15947  lgsquadlem1  15950  lgsquadlem2  15951  lgsquadlem3  15952  lgsquad2lem1  15954  m1lgs  15958  2lgslem3a  15966  2lgslem3b  15967  2lgslem3c  15968  2lgslem3d  15969  2sqlem8  15996  opvtxov  16018  opiedgov  16021  structiedg0val  16035  edgov  16058  edg0iedg0g  16061  upgredg  16139  usgrf1oedg  16200  ushgredgedg  16221  ushgredgedgloop  16223  griedg0ssusgr  16246  subgrprop3  16257  0uhgrsubgr  16260  vtxdgfval  16283  vtxdfifiun  16292  vtxdumgrfival  16293  vtxd0nedgbfi  16294  1hevtxdg1en  16303  upgriswlkdc  16355  wlkres  16374  trlreslem  16384  clwwlkn2  16416  eupthvdres  16470  eupth2lem3fi  16471  ex-ceil  16494  depindlem1  16501  qdencn  16807  cvgcmp2nlemabs  16816  trilpolemlt1  16825  nconstwlpolem0  16849  gfsump1  16868  gfsumcl  16870