Theorem eqtrid 2252

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 2240	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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  eqtr2id  2253  eqtr3id  2254  3eqtr3a  2264  3eqtr4g  2265  csbtt  3113  csbvarg  3129  csbie2g  3152  rabbi2dva  3389  csbprc  3514  disjssun  3532  disjpr2  3707  prprc2  3752  difprsn2  3784  opprc  3854  intsng  3933  riinm  4014  iinxsng  4015  iunxprg  4022  rintm  4034  sucprc  4477  unisucg  4479  xpriindim  4834  relop  4846  dmxpm  4917  riinint  4958  resabs1  5007  resabs2  5009  resima2  5012  xpssres  5013  resopab2  5025  mptimass  5054  imasng  5066  ndmima  5078  xpdisj1  5126  xpdisj2  5127  djudisj  5129  resdisj  5130  rnxpm  5131  xpima1  5148  xpima2m  5149  dmsnsnsng  5179  rnsnopg  5180  rnpropg  5181  mptiniseg  5196  dfco2a  5202  relcoi1  5233  unixpm  5237  iotaval  5262  funtp  5346  fnun  5401  fnresdisj  5405  fnima  5414  fnimaeq0  5417  fcoi1  5478  f1orescnv  5560  foun  5563  resdif  5566  tz6.12-2  5590  fveu  5591  tz6.12-1  5626  fvun2  5669  fvopab3ig  5676  f1oresrab  5768  dfmptg  5782  funopsn  5785  ressnop0  5788  fvunsng  5801  fnsnsplitss  5806  fsnunfv  5808  fvpr1  5811  fvpr2  5812  fvpr1g  5813  fvpr2g  5814  fvtp1g  5815  fvtp2g  5816  fvtp3g  5817  fvtp2  5819  fvtp3  5820  f1oiso2  5919  riotaund  5957  ovprc  6003  resoprab2  6065  fnoprabg  6069  ovidig  6086  ovigg  6089  fvmpopr2d  6105  ov6g  6107  ovconst2  6121  offval2  6197  ot1stg  6261  ot2ndg  6262  ot3rdgg  6263  fmpoco  6325  algrflemg  6339  tpostpos2  6374  rdgisuc1  6493  frec0g  6506  frecsuclem  6515  frecrdg  6517  oasuc  6573  oa1suc  6576  omsuc  6581  nnm1  6634  nnm2  6635  dfec2  6646  errn  6665  ixpsnval  6811  ixpintm  6835  mapen  6968  xpmapenlem  6971  phplem2  6975  undifdc  7047  prfidceq  7051  fisseneq  7057  ssfirab  7059  eqinfti  7148  infvalti  7150  infsnti  7158  casef  7216  caseinl  7219  caseinr  7220  djudom  7221  ctssdccl  7239  nninfwlpoimlemginf  7304  exmidfodomrlemim  7340  1qec  7536  mulidnq  7537  addpinq1  7612  suplocexprlem2b  7862  suplocexprlemlub  7872  0idsr  7915  1idsr  7916  caucvgsrlemoffres  7948  caucvgsr  7950  mulresr  7986  pitonnlem2  7995  ax1rid  8025  axcnre  8029  negid  8354  subneg  8356  negneg  8357  dfinfre  9064  2times  9199  infrenegsupex  9750  rexneg  9987  xaddpnf2  10004  xaddmnf1  10005  xaddmnf2  10006  fseq1p1m1  10251  fzosplitprm1  10400  intfracq  10502  frec2uz0d  10581  frec2uzrdg  10591  frecuzrdg0  10595  frecuzrdgg  10598  frecuzrdg0t  10604  seq3val  10642  seqvalcd  10643  iseqf1olemjpcl  10690  iseqf1olemqpcl  10691  iseqf1olemfvp  10692  seq3f1olemqsum  10695  seqf1oglem2  10702  sqval  10779  iexpcyc  10826  binom3  10839  faclbnd  10923  faclbnd2  10924  bcn1  10940  hashinfom  10960  hashennn  10962  hashxp  11008  csbwrdg  11060  ccatlid  11100  s1val  11109  swrd00g  11140  pfxclz  11170  pfxccatpfx2  11228  shftlem  11242  shftuz  11243  shftidt  11259  reim0  11287  remullem  11297  resqrexlemf1  11434  resqrexlemcalc3  11442  absexpzap  11506  absimle  11510  amgm2  11544  minmax  11656  mingeb  11668  2zinfmin  11669  xrmaxiflemval  11676  xrmaxadd  11687  infxrnegsupex  11689  xrminmax  11691  summodc  11809  fsum3  11813  sumsnf  11835  sumsns  11841  isumclim3  11849  isumge0  11856  fsump1i  11859  fsum2dlemstep  11860  fisumcom2  11864  fsumshftm  11871  fsumconst  11880  fsumiun  11903  hashrabrex  11907  hashuni  11908  binom11  11912  isumsplit  11917  geo2sum  11940  mertensabs  11963  prodmodc  12004  fprodseq  12009  prodsnf  12018  prodsns  12029  fprodconst  12046  fprod2dlemstep  12048  fprodcom2fi  12052  efgt1p2  12121  efgt1p  12122  resinval  12141  recosval  12142  cosadd  12163  ef01bndlem  12182  eirraplem  12203  bits0  12374  nninfctlemfo  12476  ialgr0  12481  algrp1  12483  eucalg  12496  phiprmpw  12659  phiprm  12660  prmdiv  12672  pythagtriplem12  12713  pythagtriplem14  12715  pythagtriplem16  12717  pceu  12733  pcfac  12788  prmpwdvds  12793  4sqlem5  12820  mul4sqlem  12831  ennnfonelem0  12891  ennnfonelemfun  12903  ennnfonelemf1  12904  ennnfonelemrn  12905  ctinfomlemom  12913  nninfdclemp1  12936  ndxid  12971  setsfun0  12983  setsresg  12985  setscom  12987  strslfv2d  12990  basm  13008  ressval3d  13019  resseqnbasd  13020  prdsval  13220  pwsval  13238  pwsplusgval  13242  pwsmulrval  13243  imasaddvallemg  13262  xpsval  13299  plusffvalg  13309  mgm1  13317  grpidvalg  13320  sgrp1  13358  prdsidlem  13394  mnd1  13402  mnd1id  13403  subsubm  13430  grppropstrg  13466  grpinvfvalg  13489  grpsubfvalg  13492  grp1  13553  prdsinvlem  13555  pwsinvg  13559  mulgfvalg  13572  mulgnn0gsum  13579  mulg2  13582  subsubg  13648  releqgg  13671  eqgfval  13673  conjsubg  13728  gsumfzconstf  13793  mgpvalg  13800  mgpbasg  13803  mgpscag  13804  mgptopng  13806  mgpdsg  13807  mgpress  13808  ringidvalg  13838  ring1  13936  opprvalg  13946  opprmulfvalg  13947  opprbasg  13952  oppraddg  13953  subsubrng  14091  subsubrg  14122  rrgval  14139  scaffvalg  14183  lmodpropd  14226  lsssetm  14233  lsslss  14258  lspfval  14265  sraring  14326  lidlvalg  14348  rspvalg  14349  lidlss  14353  islidlm  14356  lidl0cl  14360  lidlacl  14361  lidlnegcl  14362  lidl0  14366  lidl1  14367  rspcl  14368  rspssid  14369  rsp0  14370  rspssp  14371  2idlval  14379  2idlvalg  14380  crngridl  14407  rspsn  14411  zrhval  14494  zrhvalg  14495  zlmval  14504  zlmbasg  14506  zlmplusgg  14507  zlmmulrg  14508  znval  14513  znzrh2  14523  znf1o  14528  psrval  14543  mplvalcoe  14567  mpl0fi  14579  mplnegfi  14582  tgidm  14661  tgrest  14756  ssidcn  14797  txcnmpt  14860  txcn  14862  blres  15021  mopnval  15029  remetdval  15134  expcn  15156  divccncfap  15177  cncfmet  15179  cncfcncntop  15180  hovergt0  15237  cnplimcim  15254  cnplimclemr  15256  limccnpcntop  15262  limccnp2cntop  15264  dvexp  15298  dvmptid  15303  dvmptfsum  15312  elply2  15322  elplyd  15328  plyaddlem1  15334  plymullem1  15335  plycjlemc  15347  sin0pilem1  15368  pilem3  15370  ef2kpi  15393  sin2pim  15400  cos2pim  15401  sinmpi  15402  cosmpi  15403  sinppi  15404  cosppi  15405  sinhalfpip  15407  sinhalfpim  15408  coshalfpip  15409  coshalfpim  15410  tangtx  15425  1cxp  15487  ecxp  15488  rplogb1  15535  rpelogb  15536  binom4  15566  0sgm  15572  fsumdvdsmul  15578  1sgmprm  15581  1sgm2ppw  15582  lgslem1  15592  gausslemma2dlem4  15656  lgseisenlem1  15662  lgseisenlem2  15663  lgseisenlem3  15664  lgseisenlem4  15665  lgseisen  15666  lgsquadlem1  15669  lgsquadlem2  15670  lgsquadlem3  15671  lgsquad2lem1  15673  m1lgs  15677  2lgslem3a  15685  2lgslem3b  15686  2lgslem3c  15687  2lgslem3d  15688  2sqlem8  15715  opvtxov  15737  opiedgov  15740  structiedg0val  15754  edgov  15774  edg0iedg0g  15777  upgredg  15848  ex-ceil  15862  qdencn  16168  cvgcmp2nlemabs  16173  trilpolemlt1  16182  nconstwlpolem0  16204