Theorem eqtrid 2279

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 2267	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 2216

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

This theorem is referenced by:  eqtr2id  2280  eqtr3id  2281  3eqtr3a  2291  3eqtr4g  2292  eqab  2369  csbtt  3153  csbvarg  3169  csbie2g  3192  rabbi2dva  3433  csbprc  3558  disjssun  3576  disjpr2  3758  rabsnif  3763  prprc2  3806  difprsn2  3839  opprc  3909  intsng  3988  riinm  4069  iinxsng  4070  iunxprg  4077  rintm  4089  sucprc  4538  unisucg  4540  xpriindim  4898  relop  4910  dmxpm  4982  riinint  5023  resabs1  5072  resabs2  5074  resima2  5077  xpssres  5078  resopab2  5090  mptimass  5119  imasng  5132  ndmima  5144  xpdisj1  5192  xpdisj2  5193  djudisj  5195  resdisj  5196  rnxpm  5197  xpima1  5214  xpima2m  5215  dmsnsnsng  5245  rnsnopg  5246  rnpropg  5247  mptiniseg  5262  dfco2a  5268  relcoi1  5299  unixpm  5303  iotaval  5329  funtp  5414  fnun  5469  fnresdisj  5473  fnima  5482  fnimaeq0  5485  fresaunres2disj  5550  fcoi1  5552  f1orescnv  5635  foun  5638  resdif  5641  tz6.12-2  5666  fveu  5667  tz6.12-1  5702  fvun2  5749  fvopab3ig  5756  f1oresrab  5847  dfmptg  5862  funopsn  5865  ressnop0  5870  fvunsng  5883  fnsnsplitss  5888  fsnunfv  5890  fvpr1  5893  fvpr2  5894  fvpr1g  5895  fvpr2g  5896  fvtp1g  5897  fvtp2g  5898  fvtp3g  5899  fvtp2  5901  fvtp3  5902  f1oiso2  6006  riotaund  6048  ovprc  6094  resoprab2  6158  fnoprabg  6162  ovidig  6179  ovigg  6182  fvmpopr2d  6198  ov6g  6200  ovconst2  6214  offval2  6291  ot1stg  6359  ot2ndg  6360  ot3rdgg  6361  opabn1stprc  6402  fmpoco  6425  algrflemg  6439  suppsnopdc  6463  tpostpos2  6509  rdgisuc1  6628  frec0g  6641  frecsuclem  6650  frecrdg  6652  oasuc  6710  oa1suc  6713  omsuc  6718  nnm1  6771  nnm2  6772  dfec2  6783  errn  6802  ixpsnval  6949  ixpintm  6973  mapen  7112  xpmapenlem  7115  phplem2  7120  undifdc  7197  prfidceq  7201  fisseneq  7208  ssfirab  7210  eqinfti  7324  infvalti  7326  infsnti  7334  casef  7392  caseinl  7395  caseinr  7396  djudom  7397  ctssdccl  7415  nninfwlpoimlemginf  7480  exmidfodomrlemim  7517  1qec  7719  mulidnq  7720  addpinq1  7795  suplocexprlem2b  8045  suplocexprlemlub  8055  0idsr  8098  1idsr  8099  caucvgsrlemoffres  8131  caucvgsr  8133  mulresr  8169  pitonnlem2  8178  ax1rid  8208  axcnre  8212  negid  8536  subneg  8538  negneg  8539  dfinfre  9247  2times  9382  infrenegsupex  9944  rexneg  10182  xaddpnf2  10199  xaddmnf1  10200  xaddmnf2  10201  fseq1p1m1  10450  fzosplitprm1  10602  infssfzcldc  10618  infssfzledc  10619  intfracq  10706  frec2uz0d  10785  frec2uzrdg  10795  frecuzrdg0  10799  frecuzrdgg  10802  frecuzrdg0t  10808  seq3val  10846  seqvalcd  10847  iseqf1olemjpcl  10894  iseqf1olemqpcl  10895  iseqf1olemfvp  10896  seq3f1olemqsum  10899  seqf1oglem2  10906  sqval  10983  iexpcyc  11030  binom3  11043  faclbnd  11128  faclbnd2  11129  bcn1  11145  hashinfom  11166  hashennn  11168  hashxp  11216  hashfibclem  11231  hashfibc  11232  hashtpgim  11242  hashtpglem  11243  hashtpg  11244  csbwrdg  11279  ccatlid  11319  s1val  11330  swrd00g  11366  pfxclz  11396  pfxccatpfx2  11454  cats1fvn  11481  cats1fvd  11483  cats1lend  11484  shftlem  11526  shftuz  11527  shftidt  11543  reim0  11571  remullem  11581  resqrexlemf1  11718  resqrexlemcalc3  11726  absexpzap  11790  absimle  11794  amgm2  11828  minmax  11940  mingeb  11952  2zinfmin  11953  xrmaxiflemval  11960  xrmaxadd  11971  infxrnegsupex  11973  xrminmax  11975  summodc  12094  fsum3  12098  sumsnf  12120  sumsns  12126  isumclim3  12134  isumge0  12141  fsump1i  12144  fsum2dlemstep  12145  fisumcom2  12149  fsumshftm  12156  fsumconst  12165  fsumiun  12188  hashrabrex  12192  hashuni  12193  binom11  12197  isumsplit  12202  geo2sum  12225  mertensabs  12248  prodmodc  12289  fprodseq  12294  prodsnf  12303  prodsns  12314  fprodconst  12331  fprod2dlemstep  12333  fprodcom2fi  12337  efgt1p2  12406  efgt1p  12407  resinval  12426  recosval  12427  cosadd  12448  ef01bndlem  12467  eirraplem  12488  bits0  12659  nninfctlemfo  12761  ialgr0  12766  algrp1  12768  eucalg  12781  phiprmpw  12944  phiprm  12945  prmdiv  12957  pythagtriplem12  12998  pythagtriplem14  13000  pythagtriplem16  13002  pceu  13018  pcfac  13073  prmpwdvds  13078  4sqlem5  13105  mul4sqlem  13116  ballotfilem4  13185  ballotfilem1c  13195  ballotfilemgun  13212  ennnfonelem0  13240  ennnfonelemfun  13252  ennnfonelemf1  13253  ennnfonelemrn  13254  ctinfomlemom  13262  nninfdclemp1  13285  ndxid  13320  setsfun0  13332  setsresg  13334  setscom  13336  strslfv2d  13339  basm  13358  ressval3d  13369  resseqnbasd  13370  imasaddvallemg  13579  plusffvalg  13625  mgm1  13633  grpidvalg  13636  sgrp1  13674  mnd1  13710  mnd1id  13711  subsubm  13738  grppropstrg  13774  grpinvfvalg  13797  grpsubfvalg  13800  grp1  13861  mulgfvalg  13874  mulgnn0gsum  13881  mulg2  13884  subsubg  13950  releqgg  13973  eqgfval  13975  conjsubg  14030  gsumfzconstf  14095  gfsump1  14108  gfsumcl  14110  prdsval  14115  prdsidlem  14135  prdsinvlem  14138  xpsval  14143  pwsval  14146  pwsplusgval  14150  pwsmulrval  14151  pwsinvg  14157  mgpvalg  14162  mgpbasg  14165  mgpscag  14166  mgptopng  14168  mgpdsg  14169  mgpress  14170  ringidvalg  14204  ring1  14302  opprvalg  14312  opprmulfvalg  14313  opprbasg  14318  oppraddg  14319  subsubrng  14460  subsubrg  14491  rrgval  14508  scaffvalg  14580  lmodpropd  14623  lsssetm  14630  lsslss  14655  lspfval  14662  sraring  14723  lidlvalg  14745  rspvalg  14746  lidlss  14750  islidlm  14753  lidl0cl  14757  lidlacl  14758  lidlnegcl  14759  lidl0  14763  lidl1  14764  rspcl  14765  rspssid  14766  rsp0  14767  rspssp  14768  2idlval  14776  2idlvalg  14777  crngridl  14804  rspsn  14808  zrhval  14891  zrhvalg  14892  zlmval  14901  zlmbasg  14903  zlmplusgg  14904  zlmmulrg  14905  znval  14910  znzrh2  14920  znf1o  14925  psrval  14940  mplvalcoe  14971  mpl0fi  14983  mplnegfi  14986  tgidm  15065  tgrest  15160  ssidcn  15201  txcnmpt  15264  txcn  15266  blres  15425  mopnval  15433  remetdval  15538  expcn  15560  divccncfap  15581  cncfmet  15583  cncfcncntop  15584  hovergt0  15641  cnplimcim  15658  cnplimclemr  15660  limccnpcntop  15666  limccnp2cntop  15668  dvexp  15702  dvmptid  15707  dvmptfsum  15716  elply2  15726  elplyd  15732  plyaddlem1  15738  plymullem1  15739  plycjlemc  15751  sin0pilem1  15772  pilem3  15774  ef2kpi  15797  sin2pim  15804  cos2pim  15805  sinmpi  15806  cosmpi  15807  sinppi  15808  cosppi  15809  sinhalfpip  15811  sinhalfpim  15812  coshalfpip  15813  coshalfpim  15814  tangtx  15829  1cxp  15891  ecxp  15892  rplogb1  15939  rpelogb  15940  binom4  15970  0sgm  15979  fsumdvdsmul  15985  1sgmprm  15988  1sgm2ppw  15989  lgslem1  15999  gausslemma2dlem4  16063  lgseisenlem1  16069  lgseisenlem2  16070  lgseisenlem3  16071  lgseisenlem4  16072  lgseisen  16073  lgsquadlem1  16076  lgsquadlem2  16077  lgsquadlem3  16078  lgsquad2lem1  16080  m1lgs  16084  2lgslem3a  16092  2lgslem3b  16093  2lgslem3c  16094  2lgslem3d  16095  2sqlem8  16122  opvtxov  16144  opiedgov  16147  structiedg0val  16161  edgov  16184  edg0iedg0g  16187  upgredg  16265  usgrf1oedg  16326  ushgredgedg  16347  ushgredgedgloop  16349  griedg0ssusgr  16372  subgrprop3  16383  0uhgrsubgr  16386  vtxdgfval  16409  vtxdfifiun  16418  vtxdumgrfival  16419  vtxd0nedgbfi  16420  1hevtxdg1en  16429  upgriswlkdc  16481  wlkres  16500  trlreslem  16510  clwwlkn2  16542  eupthvdres  16596  eupth2lem3fi  16597  ex-ceil  16620  depindlem1  16627  qdencn  16933  cvgcmp2nlemabs  16942  trilpolemlt1  16951  nconstwlpolem0  16975