Theorem eqtrid 2220

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

Syntax hints:   -> wi 4   = wceq 1353

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 1445  ax-gen 1447  ax-4 1508  ax-17 1524  ax-ext 2157

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

This theorem is referenced by:  eqtr2id  2221  eqtr3id  2222  3eqtr3a  2232  3eqtr4g  2233  csbtt  3067  csbvarg  3083  csbie2g  3105  rabbi2dva  3341  csbprc  3466  disjssun  3484  disjpr2  3653  prprc2  3698  difprsn2  3729  opprc  3795  intsng  3874  riinm  3954  iinxsng  3955  iunxprg  3962  rintm  3974  sucprc  4406  unisucg  4408  xpriindim  4758  relop  4770  dmxpm  4840  riinint  4881  resabs1  4929  resabs2  4931  resima2  4934  xpssres  4935  resopab2  4947  imasng  4986  ndmima  4998  xpdisj1  5045  xpdisj2  5046  djudisj  5048  resdisj  5049  rnxpm  5050  xpima1  5067  xpima2m  5068  dmsnsnsng  5098  rnsnopg  5099  rnpropg  5100  mptiniseg  5115  dfco2a  5121  relcoi1  5152  unixpm  5156  iotaval  5181  funtp  5261  fnun  5314  fnresdisj  5318  fnima  5326  fnimaeq0  5329  fcoi1  5388  f1orescnv  5469  foun  5472  resdif  5475  tz6.12-2  5498  fveu  5499  tz6.12-1  5534  fvun2  5575  fvopab3ig  5582  f1oresrab  5673  dfmptg  5687  ressnop0  5689  fvunsng  5702  fnsnsplitss  5707  fsnunfv  5709  fvpr1  5712  fvpr2  5713  fvpr1g  5714  fvpr2g  5715  fvtp1g  5716  fvtp2g  5717  fvtp3g  5718  fvtp2  5720  fvtp3  5721  f1oiso2  5818  riotaund  5855  ovprc  5900  resoprab2  5962  fnoprabg  5966  ovidig  5982  ovigg  5985  ov6g  6002  ovconst2  6016  offval2  6088  ot1stg  6143  ot2ndg  6144  ot3rdgg  6145  fmpoco  6207  algrflemg  6221  tpostpos2  6256  rdgisuc1  6375  frec0g  6388  frecsuclem  6397  frecrdg  6399  oasuc  6455  oa1suc  6458  omsuc  6463  nnm1  6516  nnm2  6517  dfec2  6528  errn  6547  ixpsnval  6691  ixpintm  6715  mapen  6836  xpmapenlem  6839  phplem2  6843  undifdc  6913  fisseneq  6921  ssfirab  6923  eqinfti  7009  infvalti  7011  infsnti  7019  casef  7077  caseinl  7080  caseinr  7081  djudom  7082  ctssdccl  7100  nninfwlpoimlemginf  7164  exmidfodomrlemim  7190  1qec  7362  mulidnq  7363  addpinq1  7438  suplocexprlem2b  7688  suplocexprlemlub  7698  0idsr  7741  1idsr  7742  caucvgsrlemoffres  7774  caucvgsr  7776  mulresr  7812  pitonnlem2  7821  ax1rid  7851  axcnre  7855  negid  8178  subneg  8180  negneg  8181  dfinfre  8884  2times  9018  infrenegsupex  9565  rexneg  9799  xaddpnf2  9816  xaddmnf1  9817  xaddmnf2  9818  fseq1p1m1  10062  fzosplitprm1  10202  intfracq  10288  frec2uz0d  10367  frec2uzrdg  10377  frecuzrdg0  10381  frecuzrdgg  10384  frecuzrdg0t  10390  seq3val  10426  seqvalcd  10427  iseqf1olemjpcl  10463  iseqf1olemqpcl  10464  iseqf1olemfvp  10465  seq3f1olemqsum  10468  sqval  10546  iexpcyc  10592  binom3  10605  faclbnd  10687  faclbnd2  10688  bcn1  10704  hashinfom  10724  hashennn  10726  hashxp  10772  shftlem  10791  shftuz  10792  shftidt  10808  reim0  10836  remullem  10846  resqrexlemf1  10983  resqrexlemcalc3  10991  absexpzap  11055  absimle  11059  amgm2  11093  minmax  11204  mingeb  11216  2zinfmin  11217  xrmaxiflemval  11224  xrmaxadd  11235  infxrnegsupex  11237  xrminmax  11239  summodc  11357  fsum3  11361  sumsnf  11383  sumsns  11389  isumclim3  11397  isumge0  11404  fsump1i  11407  fsum2dlemstep  11408  fisumcom2  11412  fsumshftm  11419  fsumconst  11428  fsumiun  11451  hashrabrex  11455  hashuni  11456  binom11  11460  isumsplit  11465  geo2sum  11488  mertensabs  11511  prodmodc  11552  fprodseq  11557  prodsnf  11566  prodsns  11577  fprodconst  11594  fprod2dlemstep  11596  fprodcom2fi  11600  efgt1p2  11669  efgt1p  11670  resinval  11689  recosval  11690  cosadd  11711  ef01bndlem  11730  eirraplem  11750  ialgr0  12009  algrp1  12011  eucalg  12024  phiprmpw  12187  phiprm  12188  prmdiv  12200  pythagtriplem12  12240  pythagtriplem14  12242  pythagtriplem16  12244  pceu  12260  pcfac  12313  prmpwdvds  12318  4sqlem5  12345  mul4sqlem  12356  ennnfonelem0  12371  ennnfonelemfun  12383  ennnfonelemf1  12384  ennnfonelemrn  12385  ctinfomlemom  12393  nninfdclemp1  12416  ndxid  12451  setsfun0  12463  setsresg  12465  setscom  12467  strslfv2d  12469  ressid2  12488  ressval2  12489  plusffvalg  12645  mgm1  12653  grpidvalg  12656  sgrp1  12680  mnd1  12708  mnd1id  12709  grppropstrg  12755  grpinvfvalg  12775  grpsubfvalg  12778  grp1  12835  mulgfvalg  12844  mulg2  12851  mgpvalg  12928  mgpbasg  12930  mgpscag  12931  mgptopng  12933  mgpdsg  12934  ringidvalg  12937  ring1  13028  tgidm  13125  tgrest  13220  ssidcn  13261  txcnmpt  13324  txcn  13326  blres  13485  mopnval  13493  remetdval  13590  divccncfap  13628  cncfmet  13630  cncfcncntop  13631  cnplimcim  13687  cnplimclemr  13689  limccnpcntop  13695  limccnp2cntop  13697  dvexp  13726  sin0pilem1  13753  pilem3  13755  ef2kpi  13778  sin2pim  13785  cos2pim  13786  sinmpi  13787  cosmpi  13788  sinppi  13789  cosppi  13790  sinhalfpip  13792  sinhalfpim  13793  coshalfpip  13794  coshalfpim  13795  tangtx  13810  1cxp  13872  ecxp  13873  rplogb1  13917  rpelogb  13918  binom4  13948  lgslem1  13952  2sqlem8  14010  ex-ceil  14018  qdencn  14316  cvgcmp2nlemabs  14321  trilpolemlt1  14330  nconstwlpolem0  14351