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  5826  funopsn  5829  ressnop0  5834  fvunsng  5847  fnsnsplitss  5852  fsnunfv  5854  fvpr1  5857  fvpr2  5858  fvpr1g  5859  fvpr2g  5860  fvtp1g  5861  fvtp2g  5862  fvtp3g  5863  fvtp2  5865  fvtp3  5866  f1oiso2  5967  riotaund  6007  ovprc  6053  resoprab2  6117  fnoprabg  6121  ovidig  6138  ovigg  6141  fvmpopr2d  6157  ov6g  6159  ovconst2  6173  offval2  6250  ot1stg  6314  ot2ndg  6315  ot3rdgg  6316  opabn1stprc  6357  fmpoco  6380  algrflemg  6394  tpostpos2  6430  rdgisuc1  6549  frec0g  6562  frecsuclem  6571  frecrdg  6573  oasuc  6631  oa1suc  6634  omsuc  6639  nnm1  6692  nnm2  6693  dfec2  6704  errn  6723  ixpsnval  6869  ixpintm  6893  mapen  7031  xpmapenlem  7034  phplem2  7038  undifdc  7115  prfidceq  7119  fisseneq  7126  ssfirab  7128  eqinfti  7218  infvalti  7220  infsnti  7228  casef  7286  caseinl  7289  caseinr  7290  djudom  7291  ctssdccl  7309  nninfwlpoimlemginf  7374  exmidfodomrlemim  7411  1qec  7607  mulidnq  7608  addpinq1  7683  suplocexprlem2b  7933  suplocexprlemlub  7943  0idsr  7986  1idsr  7987  caucvgsrlemoffres  8019  caucvgsr  8021  mulresr  8057  pitonnlem2  8066  ax1rid  8096  axcnre  8100  negid  8425  subneg  8427  negneg  8428  dfinfre  9135  2times  9270  infrenegsupex  9827  rexneg  10064  xaddpnf2  10081  xaddmnf1  10082  xaddmnf2  10083  fseq1p1m1  10328  fzosplitprm1  10479  intfracq  10581  frec2uz0d  10660  frec2uzrdg  10670  frecuzrdg0  10674  frecuzrdgg  10677  frecuzrdg0t  10683  seq3val  10721  seqvalcd  10722  iseqf1olemjpcl  10769  iseqf1olemqpcl  10770  iseqf1olemfvp  10771  seq3f1olemqsum  10774  seqf1oglem2  10781  sqval  10858  iexpcyc  10905  binom3  10918  faclbnd  11002  faclbnd2  11003  bcn1  11019  hashinfom  11039  hashennn  11041  hashxp  11089  csbwrdg  11142  ccatlid  11182  s1val  11193  swrd00g  11229  pfxclz  11259  pfxccatpfx2  11317  cats1fvn  11344  cats1fvd  11346  cats1lend  11347  shftlem  11376  shftuz  11377  shftidt  11393  reim0  11421  remullem  11431  resqrexlemf1  11568  resqrexlemcalc3  11576  absexpzap  11640  absimle  11644  amgm2  11678  minmax  11790  mingeb  11802  2zinfmin  11803  xrmaxiflemval  11810  xrmaxadd  11821  infxrnegsupex  11823  xrminmax  11825  summodc  11943  fsum3  11947  sumsnf  11969  sumsns  11975  isumclim3  11983  isumge0  11990  fsump1i  11993  fsum2dlemstep  11994  fisumcom2  11998  fsumshftm  12005  fsumconst  12014  fsumiun  12037  hashrabrex  12041  hashuni  12042  binom11  12046  isumsplit  12051  geo2sum  12074  mertensabs  12097  prodmodc  12138  fprodseq  12143  prodsnf  12152  prodsns  12163  fprodconst  12180  fprod2dlemstep  12182  fprodcom2fi  12186  efgt1p2  12255  efgt1p  12256  resinval  12275  recosval  12276  cosadd  12297  ef01bndlem  12316  eirraplem  12337  bits0  12508  nninfctlemfo  12610  ialgr0  12615  algrp1  12617  eucalg  12630  phiprmpw  12793  phiprm  12794  prmdiv  12806  pythagtriplem12  12847  pythagtriplem14  12849  pythagtriplem16  12851  pceu  12867  pcfac  12922  prmpwdvds  12927  4sqlem5  12954  mul4sqlem  12965  ennnfonelem0  13025  ennnfonelemfun  13037  ennnfonelemf1  13038  ennnfonelemrn  13039  ctinfomlemom  13047  nninfdclemp1  13070  ndxid  13105  setsfun0  13117  setsresg  13119  setscom  13121  strslfv2d  13124  basm  13143  ressval3d  13154  resseqnbasd  13155  prdsval  13355  pwsval  13373  pwsplusgval  13377  pwsmulrval  13378  imasaddvallemg  13397  xpsval  13434  plusffvalg  13444  mgm1  13452  grpidvalg  13455  sgrp1  13493  prdsidlem  13529  mnd1  13537  mnd1id  13538  subsubm  13565  grppropstrg  13601  grpinvfvalg  13624  grpsubfvalg  13627  grp1  13688  prdsinvlem  13690  pwsinvg  13694  mulgfvalg  13707  mulgnn0gsum  13714  mulg2  13717  subsubg  13783  releqgg  13806  eqgfval  13808  conjsubg  13863  gsumfzconstf  13928  mgpvalg  13935  mgpbasg  13938  mgpscag  13939  mgptopng  13941  mgpdsg  13942  mgpress  13943  ringidvalg  13973  ring1  14071  opprvalg  14081  opprmulfvalg  14082  opprbasg  14087  oppraddg  14088  subsubrng  14227  subsubrg  14258  rrgval  14275  scaffvalg  14319  lmodpropd  14362  lsssetm  14369  lsslss  14394  lspfval  14401  sraring  14462  lidlvalg  14484  rspvalg  14485  lidlss  14489  islidlm  14492  lidl0cl  14496  lidlacl  14497  lidlnegcl  14498  lidl0  14502  lidl1  14503  rspcl  14504  rspssid  14505  rsp0  14506  rspssp  14507  2idlval  14515  2idlvalg  14516  crngridl  14543  rspsn  14547  zrhval  14630  zrhvalg  14631  zlmval  14640  zlmbasg  14642  zlmplusgg  14643  zlmmulrg  14644  znval  14649  znzrh2  14659  znf1o  14664  psrval  14679  mplvalcoe  14703  mpl0fi  14715  mplnegfi  14718  tgidm  14797  tgrest  14892  ssidcn  14933  txcnmpt  14996  txcn  14998  blres  15157  mopnval  15165  remetdval  15270  expcn  15292  divccncfap  15313  cncfmet  15315  cncfcncntop  15316  hovergt0  15373  cnplimcim  15390  cnplimclemr  15392  limccnpcntop  15398  limccnp2cntop  15400  dvexp  15434  dvmptid  15439  dvmptfsum  15448  elply2  15458  elplyd  15464  plyaddlem1  15470  plymullem1  15471  plycjlemc  15483  sin0pilem1  15504  pilem3  15506  ef2kpi  15529  sin2pim  15536  cos2pim  15537  sinmpi  15538  cosmpi  15539  sinppi  15540  cosppi  15541  sinhalfpip  15543  sinhalfpim  15544  coshalfpip  15545  coshalfpim  15546  tangtx  15561  1cxp  15623  ecxp  15624  rplogb1  15671  rpelogb  15672  binom4  15702  0sgm  15708  fsumdvdsmul  15714  1sgmprm  15717  1sgm2ppw  15718  lgslem1  15728  gausslemma2dlem4  15792  lgseisenlem1  15798  lgseisenlem2  15799  lgseisenlem3  15800  lgseisenlem4  15801  lgseisen  15802  lgsquadlem1  15805  lgsquadlem2  15806  lgsquadlem3  15807  lgsquad2lem1  15809  m1lgs  15813  2lgslem3a  15821  2lgslem3b  15822  2lgslem3c  15823  2lgslem3d  15824  2sqlem8  15851  opvtxov  15873  opiedgov  15876  structiedg0val  15890  edgov  15913  edg0iedg0g  15916  upgredg  15994  usgrf1oedg  16055  ushgredgedg  16076  ushgredgedgloop  16078  griedg0ssusgr  16101  subgrprop3  16112  0uhgrsubgr  16115  vtxdgfval  16138  vtxdfifiun  16147  vtxdumgrfival  16148  vtxd0nedgbfi  16149  1hevtxdg1en  16158  upgriswlkdc  16210  wlkres  16229  trlreslem  16239  clwwlkn2  16271  ex-ceil  16322  qdencn  16631  cvgcmp2nlemabs  16636  trilpolemlt1  16645  nconstwlpolem0  16667