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  5508  f1orescnv  5590  foun  5593  resdif  5596  tz6.12-2  5620  fveu  5621  tz6.12-1  5656  fvun2  5703  fvopab3ig  5710  f1oresrab  5802  dfmptg  5816  funopsn  5819  ressnop0  5824  fvunsng  5837  fnsnsplitss  5842  fsnunfv  5844  fvpr1  5847  fvpr2  5848  fvpr1g  5849  fvpr2g  5850  fvtp1g  5851  fvtp2g  5852  fvtp3g  5853  fvtp2  5855  fvtp3  5856  f1oiso2  5957  riotaund  5997  ovprc  6043  resoprab2  6107  fnoprabg  6111  ovidig  6128  ovigg  6131  fvmpopr2d  6147  ov6g  6149  ovconst2  6163  offval2  6240  ot1stg  6304  ot2ndg  6305  ot3rdgg  6306  fmpoco  6368  algrflemg  6382  tpostpos2  6417  rdgisuc1  6536  frec0g  6549  frecsuclem  6558  frecrdg  6560  oasuc  6618  oa1suc  6621  omsuc  6626  nnm1  6679  nnm2  6680  dfec2  6691  errn  6710  ixpsnval  6856  ixpintm  6880  mapen  7015  xpmapenlem  7018  phplem2  7022  undifdc  7097  prfidceq  7101  fisseneq  7107  ssfirab  7109  eqinfti  7198  infvalti  7200  infsnti  7208  casef  7266  caseinl  7269  caseinr  7270  djudom  7271  ctssdccl  7289  nninfwlpoimlemginf  7354  exmidfodomrlemim  7390  1qec  7586  mulidnq  7587  addpinq1  7662  suplocexprlem2b  7912  suplocexprlemlub  7922  0idsr  7965  1idsr  7966  caucvgsrlemoffres  7998  caucvgsr  8000  mulresr  8036  pitonnlem2  8045  ax1rid  8075  axcnre  8079  negid  8404  subneg  8406  negneg  8407  dfinfre  9114  2times  9249  infrenegsupex  9801  rexneg  10038  xaddpnf2  10055  xaddmnf1  10056  xaddmnf2  10057  fseq1p1m1  10302  fzosplitprm1  10452  intfracq  10554  frec2uz0d  10633  frec2uzrdg  10643  frecuzrdg0  10647  frecuzrdgg  10650  frecuzrdg0t  10656  seq3val  10694  seqvalcd  10695  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  iseqf1olemfvp  10744  seq3f1olemqsum  10747  seqf1oglem2  10754  sqval  10831  iexpcyc  10878  binom3  10891  faclbnd  10975  faclbnd2  10976  bcn1  10992  hashinfom  11012  hashennn  11014  hashxp  11061  csbwrdg  11114  ccatlid  11154  s1val  11165  swrd00g  11197  pfxclz  11227  pfxccatpfx2  11285  cats1fvn  11312  cats1fvd  11314  cats1lend  11315  shftlem  11343  shftuz  11344  shftidt  11360  reim0  11388  remullem  11398  resqrexlemf1  11535  resqrexlemcalc3  11543  absexpzap  11607  absimle  11611  amgm2  11645  minmax  11757  mingeb  11769  2zinfmin  11770  xrmaxiflemval  11777  xrmaxadd  11788  infxrnegsupex  11790  xrminmax  11792  summodc  11910  fsum3  11914  sumsnf  11936  sumsns  11942  isumclim3  11950  isumge0  11957  fsump1i  11960  fsum2dlemstep  11961  fisumcom2  11965  fsumshftm  11972  fsumconst  11981  fsumiun  12004  hashrabrex  12008  hashuni  12009  binom11  12013  isumsplit  12018  geo2sum  12041  mertensabs  12064  prodmodc  12105  fprodseq  12110  prodsnf  12119  prodsns  12130  fprodconst  12147  fprod2dlemstep  12149  fprodcom2fi  12153  efgt1p2  12222  efgt1p  12223  resinval  12242  recosval  12243  cosadd  12264  ef01bndlem  12283  eirraplem  12304  bits0  12475  nninfctlemfo  12577  ialgr0  12582  algrp1  12584  eucalg  12597  phiprmpw  12760  phiprm  12761  prmdiv  12773  pythagtriplem12  12814  pythagtriplem14  12816  pythagtriplem16  12818  pceu  12834  pcfac  12889  prmpwdvds  12894  4sqlem5  12921  mul4sqlem  12932  ennnfonelem0  12992  ennnfonelemfun  13004  ennnfonelemf1  13005  ennnfonelemrn  13006  ctinfomlemom  13014  nninfdclemp1  13037  ndxid  13072  setsfun0  13084  setsresg  13086  setscom  13088  strslfv2d  13091  basm  13110  ressval3d  13121  resseqnbasd  13122  prdsval  13322  pwsval  13340  pwsplusgval  13344  pwsmulrval  13345  imasaddvallemg  13364  xpsval  13401  plusffvalg  13411  mgm1  13419  grpidvalg  13422  sgrp1  13460  prdsidlem  13496  mnd1  13504  mnd1id  13505  subsubm  13532  grppropstrg  13568  grpinvfvalg  13591  grpsubfvalg  13594  grp1  13655  prdsinvlem  13657  pwsinvg  13661  mulgfvalg  13674  mulgnn0gsum  13681  mulg2  13684  subsubg  13750  releqgg  13773  eqgfval  13775  conjsubg  13830  gsumfzconstf  13895  mgpvalg  13902  mgpbasg  13905  mgpscag  13906  mgptopng  13908  mgpdsg  13909  mgpress  13910  ringidvalg  13940  ring1  14038  opprvalg  14048  opprmulfvalg  14049  opprbasg  14054  oppraddg  14055  subsubrng  14194  subsubrg  14225  rrgval  14242  scaffvalg  14286  lmodpropd  14329  lsssetm  14336  lsslss  14361  lspfval  14368  sraring  14429  lidlvalg  14451  rspvalg  14452  lidlss  14456  islidlm  14459  lidl0cl  14463  lidlacl  14464  lidlnegcl  14465  lidl0  14469  lidl1  14470  rspcl  14471  rspssid  14472  rsp0  14473  rspssp  14474  2idlval  14482  2idlvalg  14483  crngridl  14510  rspsn  14514  zrhval  14597  zrhvalg  14598  zlmval  14607  zlmbasg  14609  zlmplusgg  14610  zlmmulrg  14611  znval  14616  znzrh2  14626  znf1o  14631  psrval  14646  mplvalcoe  14670  mpl0fi  14682  mplnegfi  14685  tgidm  14764  tgrest  14859  ssidcn  14900  txcnmpt  14963  txcn  14965  blres  15124  mopnval  15132  remetdval  15237  expcn  15259  divccncfap  15280  cncfmet  15282  cncfcncntop  15283  hovergt0  15340  cnplimcim  15357  cnplimclemr  15359  limccnpcntop  15365  limccnp2cntop  15367  dvexp  15401  dvmptid  15406  dvmptfsum  15415  elply2  15425  elplyd  15431  plyaddlem1  15437  plymullem1  15438  plycjlemc  15450  sin0pilem1  15471  pilem3  15473  ef2kpi  15496  sin2pim  15503  cos2pim  15504  sinmpi  15505  cosmpi  15506  sinppi  15507  cosppi  15508  sinhalfpip  15510  sinhalfpim  15511  coshalfpip  15512  coshalfpim  15513  tangtx  15528  1cxp  15590  ecxp  15591  rplogb1  15638  rpelogb  15639  binom4  15669  0sgm  15675  fsumdvdsmul  15681  1sgmprm  15684  1sgm2ppw  15685  lgslem1  15695  gausslemma2dlem4  15759  lgseisenlem1  15765  lgseisenlem2  15766  lgseisenlem3  15767  lgseisenlem4  15768  lgseisen  15769  lgsquadlem1  15772  lgsquadlem2  15773  lgsquadlem3  15774  lgsquad2lem1  15776  m1lgs  15780  2lgslem3a  15788  2lgslem3b  15789  2lgslem3c  15790  2lgslem3d  15791  2sqlem8  15818  opvtxov  15840  opiedgov  15843  structiedg0val  15857  edgov  15879  edg0iedg0g  15882  upgredg  15958  usgrf1oedg  16019  ushgredgedg  16040  ushgredgedgloop  16042  vtxdgfval  16048  vtxdfifiun  16057  vtxdumgrfival  16058  vtxd0nedgbfi  16059  upgriswlkdc  16106  wlkres  16123  trlreslem  16132  clwwlkn2  16163  ex-ceil  16173  qdencn  16483  cvgcmp2nlemabs  16488  trilpolemlt1  16497  nconstwlpolem0  16519