Theorem eqtrid 2274

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

Syntax hints:   -> wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  eqtr2id  2275  eqtr3id  2276  3eqtr3a  2286  3eqtr4g  2287  csbtt  3136  csbvarg  3152  csbie2g  3175  rabbi2dva  3412  csbprc  3537  disjssun  3555  disjpr2  3730  prprc2  3776  difprsn2  3808  opprc  3878  intsng  3957  riinm  4038  iinxsng  4039  iunxprg  4046  rintm  4058  sucprc  4503  unisucg  4505  xpriindim  4860  relop  4872  dmxpm  4944  riinint  4985  resabs1  5034  resabs2  5036  resima2  5039  xpssres  5040  resopab2  5052  mptimass  5081  imasng  5093  ndmima  5105  xpdisj1  5153  xpdisj2  5154  djudisj  5156  resdisj  5157  rnxpm  5158  xpima1  5175  xpima2m  5176  dmsnsnsng  5206  rnsnopg  5207  rnpropg  5208  mptiniseg  5223  dfco2a  5229  relcoi1  5260  unixpm  5264  iotaval  5290  funtp  5374  fnun  5429  fnresdisj  5433  fnima  5442  fnimaeq0  5445  fcoi1  5506  f1orescnv  5588  foun  5591  resdif  5594  tz6.12-2  5618  fveu  5619  tz6.12-1  5654  fvun2  5701  fvopab3ig  5708  f1oresrab  5800  dfmptg  5814  funopsn  5817  ressnop0  5820  fvunsng  5833  fnsnsplitss  5838  fsnunfv  5840  fvpr1  5843  fvpr2  5844  fvpr1g  5845  fvpr2g  5846  fvtp1g  5847  fvtp2g  5848  fvtp3g  5849  fvtp2  5851  fvtp3  5852  f1oiso2  5951  riotaund  5991  ovprc  6037  resoprab2  6101  fnoprabg  6105  ovidig  6122  ovigg  6125  fvmpopr2d  6141  ov6g  6143  ovconst2  6157  offval2  6234  ot1stg  6298  ot2ndg  6299  ot3rdgg  6300  fmpoco  6362  algrflemg  6376  tpostpos2  6411  rdgisuc1  6530  frec0g  6543  frecsuclem  6552  frecrdg  6554  oasuc  6610  oa1suc  6613  omsuc  6618  nnm1  6671  nnm2  6672  dfec2  6683  errn  6702  ixpsnval  6848  ixpintm  6872  mapen  7007  xpmapenlem  7010  phplem2  7014  undifdc  7086  prfidceq  7090  fisseneq  7096  ssfirab  7098  eqinfti  7187  infvalti  7189  infsnti  7197  casef  7255  caseinl  7258  caseinr  7259  djudom  7260  ctssdccl  7278  nninfwlpoimlemginf  7343  exmidfodomrlemim  7379  1qec  7575  mulidnq  7576  addpinq1  7651  suplocexprlem2b  7901  suplocexprlemlub  7911  0idsr  7954  1idsr  7955  caucvgsrlemoffres  7987  caucvgsr  7989  mulresr  8025  pitonnlem2  8034  ax1rid  8064  axcnre  8068  negid  8393  subneg  8395  negneg  8396  dfinfre  9103  2times  9238  infrenegsupex  9789  rexneg  10026  xaddpnf2  10043  xaddmnf1  10044  xaddmnf2  10045  fseq1p1m1  10290  fzosplitprm1  10440  intfracq  10542  frec2uz0d  10621  frec2uzrdg  10631  frecuzrdg0  10635  frecuzrdgg  10638  frecuzrdg0t  10644  seq3val  10682  seqvalcd  10683  iseqf1olemjpcl  10730  iseqf1olemqpcl  10731  iseqf1olemfvp  10732  seq3f1olemqsum  10735  seqf1oglem2  10742  sqval  10819  iexpcyc  10866  binom3  10879  faclbnd  10963  faclbnd2  10964  bcn1  10980  hashinfom  11000  hashennn  11002  hashxp  11048  csbwrdg  11101  ccatlid  11141  s1val  11150  swrd00g  11181  pfxclz  11211  pfxccatpfx2  11269  cats1fvn  11296  cats1fvd  11298  cats1lend  11299  shftlem  11327  shftuz  11328  shftidt  11344  reim0  11372  remullem  11382  resqrexlemf1  11519  resqrexlemcalc3  11527  absexpzap  11591  absimle  11595  amgm2  11629  minmax  11741  mingeb  11753  2zinfmin  11754  xrmaxiflemval  11761  xrmaxadd  11772  infxrnegsupex  11774  xrminmax  11776  summodc  11894  fsum3  11898  sumsnf  11920  sumsns  11926  isumclim3  11934  isumge0  11941  fsump1i  11944  fsum2dlemstep  11945  fisumcom2  11949  fsumshftm  11956  fsumconst  11965  fsumiun  11988  hashrabrex  11992  hashuni  11993  binom11  11997  isumsplit  12002  geo2sum  12025  mertensabs  12048  prodmodc  12089  fprodseq  12094  prodsnf  12103  prodsns  12114  fprodconst  12131  fprod2dlemstep  12133  fprodcom2fi  12137  efgt1p2  12206  efgt1p  12207  resinval  12226  recosval  12227  cosadd  12248  ef01bndlem  12267  eirraplem  12288  bits0  12459  nninfctlemfo  12561  ialgr0  12566  algrp1  12568  eucalg  12581  phiprmpw  12744  phiprm  12745  prmdiv  12757  pythagtriplem12  12798  pythagtriplem14  12800  pythagtriplem16  12802  pceu  12818  pcfac  12873  prmpwdvds  12878  4sqlem5  12905  mul4sqlem  12916  ennnfonelem0  12976  ennnfonelemfun  12988  ennnfonelemf1  12989  ennnfonelemrn  12990  ctinfomlemom  12998  nninfdclemp1  13021  ndxid  13056  setsfun0  13068  setsresg  13070  setscom  13072  strslfv2d  13075  basm  13094  ressval3d  13105  resseqnbasd  13106  prdsval  13306  pwsval  13324  pwsplusgval  13328  pwsmulrval  13329  imasaddvallemg  13348  xpsval  13385  plusffvalg  13395  mgm1  13403  grpidvalg  13406  sgrp1  13444  prdsidlem  13480  mnd1  13488  mnd1id  13489  subsubm  13516  grppropstrg  13552  grpinvfvalg  13575  grpsubfvalg  13578  grp1  13639  prdsinvlem  13641  pwsinvg  13645  mulgfvalg  13658  mulgnn0gsum  13665  mulg2  13668  subsubg  13734  releqgg  13757  eqgfval  13759  conjsubg  13814  gsumfzconstf  13879  mgpvalg  13886  mgpbasg  13889  mgpscag  13890  mgptopng  13892  mgpdsg  13893  mgpress  13894  ringidvalg  13924  ring1  14022  opprvalg  14032  opprmulfvalg  14033  opprbasg  14038  oppraddg  14039  subsubrng  14178  subsubrg  14209  rrgval  14226  scaffvalg  14270  lmodpropd  14313  lsssetm  14320  lsslss  14345  lspfval  14352  sraring  14413  lidlvalg  14435  rspvalg  14436  lidlss  14440  islidlm  14443  lidl0cl  14447  lidlacl  14448  lidlnegcl  14449  lidl0  14453  lidl1  14454  rspcl  14455  rspssid  14456  rsp0  14457  rspssp  14458  2idlval  14466  2idlvalg  14467  crngridl  14494  rspsn  14498  zrhval  14581  zrhvalg  14582  zlmval  14591  zlmbasg  14593  zlmplusgg  14594  zlmmulrg  14595  znval  14600  znzrh2  14610  znf1o  14615  psrval  14630  mplvalcoe  14654  mpl0fi  14666  mplnegfi  14669  tgidm  14748  tgrest  14843  ssidcn  14884  txcnmpt  14947  txcn  14949  blres  15108  mopnval  15116  remetdval  15221  expcn  15243  divccncfap  15264  cncfmet  15266  cncfcncntop  15267  hovergt0  15324  cnplimcim  15341  cnplimclemr  15343  limccnpcntop  15349  limccnp2cntop  15351  dvexp  15385  dvmptid  15390  dvmptfsum  15399  elply2  15409  elplyd  15415  plyaddlem1  15421  plymullem1  15422  plycjlemc  15434  sin0pilem1  15455  pilem3  15457  ef2kpi  15480  sin2pim  15487  cos2pim  15488  sinmpi  15489  cosmpi  15490  sinppi  15491  cosppi  15492  sinhalfpip  15494  sinhalfpim  15495  coshalfpip  15496  coshalfpim  15497  tangtx  15512  1cxp  15574  ecxp  15575  rplogb1  15622  rpelogb  15623  binom4  15653  0sgm  15659  fsumdvdsmul  15665  1sgmprm  15668  1sgm2ppw  15669  lgslem1  15679  gausslemma2dlem4  15743  lgseisenlem1  15749  lgseisenlem2  15750  lgseisenlem3  15751  lgseisenlem4  15752  lgseisen  15753  lgsquadlem1  15756  lgsquadlem2  15757  lgsquadlem3  15758  lgsquad2lem1  15760  m1lgs  15764  2lgslem3a  15772  2lgslem3b  15773  2lgslem3c  15774  2lgslem3d  15775  2sqlem8  15802  opvtxov  15824  opiedgov  15827  structiedg0val  15841  edgov  15863  edg0iedg0g  15866  upgredg  15942  usgrf1oedg  16003  ushgredgedg  16024  ushgredgedgloop  16026  upgriswlkdc  16071  ex-ceil  16090  qdencn  16395  cvgcmp2nlemabs  16400  trilpolemlt1  16409  nconstwlpolem0  16431