Theorem eqtrid 2222

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 2210	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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  eqtr2id  2223  eqtr3id  2224  3eqtr3a  2234  3eqtr4g  2235  csbtt  3070  csbvarg  3086  csbie2g  3108  rabbi2dva  3344  csbprc  3469  disjssun  3487  disjpr2  3657  prprc2  3702  difprsn2  3733  opprc  3800  intsng  3879  riinm  3960  iinxsng  3961  iunxprg  3968  rintm  3980  sucprc  4413  unisucg  4415  xpriindim  4766  relop  4778  dmxpm  4848  riinint  4889  resabs1  4937  resabs2  4939  resima2  4942  xpssres  4943  resopab2  4955  imasng  4994  ndmima  5006  xpdisj1  5054  xpdisj2  5055  djudisj  5057  resdisj  5058  rnxpm  5059  xpima1  5076  xpima2m  5077  dmsnsnsng  5107  rnsnopg  5108  rnpropg  5109  mptiniseg  5124  dfco2a  5130  relcoi1  5161  unixpm  5165  iotaval  5190  funtp  5270  fnun  5323  fnresdisj  5327  fnima  5335  fnimaeq0  5338  fcoi1  5397  f1orescnv  5478  foun  5481  resdif  5484  tz6.12-2  5507  fveu  5508  tz6.12-1  5543  fvun2  5584  fvopab3ig  5591  f1oresrab  5682  dfmptg  5696  ressnop0  5698  fvunsng  5711  fnsnsplitss  5716  fsnunfv  5718  fvpr1  5721  fvpr2  5722  fvpr1g  5723  fvpr2g  5724  fvtp1g  5725  fvtp2g  5726  fvtp3g  5727  fvtp2  5729  fvtp3  5730  f1oiso2  5828  riotaund  5865  ovprc  5910  resoprab2  5972  fnoprabg  5976  ovidig  5992  ovigg  5995  ov6g  6012  ovconst2  6026  offval2  6098  ot1stg  6153  ot2ndg  6154  ot3rdgg  6155  fmpoco  6217  algrflemg  6231  tpostpos2  6266  rdgisuc1  6385  frec0g  6398  frecsuclem  6407  frecrdg  6409  oasuc  6465  oa1suc  6468  omsuc  6473  nnm1  6526  nnm2  6527  dfec2  6538  errn  6557  ixpsnval  6701  ixpintm  6725  mapen  6846  xpmapenlem  6849  phplem2  6853  undifdc  6923  fisseneq  6931  ssfirab  6933  eqinfti  7019  infvalti  7021  infsnti  7029  casef  7087  caseinl  7090  caseinr  7091  djudom  7092  ctssdccl  7110  nninfwlpoimlemginf  7174  exmidfodomrlemim  7200  1qec  7387  mulidnq  7388  addpinq1  7463  suplocexprlem2b  7713  suplocexprlemlub  7723  0idsr  7766  1idsr  7767  caucvgsrlemoffres  7799  caucvgsr  7801  mulresr  7837  pitonnlem2  7846  ax1rid  7876  axcnre  7880  negid  8204  subneg  8206  negneg  8207  dfinfre  8913  2times  9047  infrenegsupex  9594  rexneg  9830  xaddpnf2  9847  xaddmnf1  9848  xaddmnf2  9849  fseq1p1m1  10094  fzosplitprm1  10234  intfracq  10320  frec2uz0d  10399  frec2uzrdg  10409  frecuzrdg0  10413  frecuzrdgg  10416  frecuzrdg0t  10422  seq3val  10458  seqvalcd  10459  iseqf1olemjpcl  10495  iseqf1olemqpcl  10496  iseqf1olemfvp  10497  seq3f1olemqsum  10500  sqval  10578  iexpcyc  10625  binom3  10638  faclbnd  10721  faclbnd2  10722  bcn1  10738  hashinfom  10758  hashennn  10760  hashxp  10806  shftlem  10825  shftuz  10826  shftidt  10842  reim0  10870  remullem  10880  resqrexlemf1  11017  resqrexlemcalc3  11025  absexpzap  11089  absimle  11093  amgm2  11127  minmax  11238  mingeb  11250  2zinfmin  11251  xrmaxiflemval  11258  xrmaxadd  11269  infxrnegsupex  11271  xrminmax  11273  summodc  11391  fsum3  11395  sumsnf  11417  sumsns  11423  isumclim3  11431  isumge0  11438  fsump1i  11441  fsum2dlemstep  11442  fisumcom2  11446  fsumshftm  11453  fsumconst  11462  fsumiun  11485  hashrabrex  11489  hashuni  11490  binom11  11494  isumsplit  11499  geo2sum  11522  mertensabs  11545  prodmodc  11586  fprodseq  11591  prodsnf  11600  prodsns  11611  fprodconst  11628  fprod2dlemstep  11630  fprodcom2fi  11634  efgt1p2  11703  efgt1p  11704  resinval  11723  recosval  11724  cosadd  11745  ef01bndlem  11764  eirraplem  11784  ialgr0  12044  algrp1  12046  eucalg  12059  phiprmpw  12222  phiprm  12223  prmdiv  12235  pythagtriplem12  12275  pythagtriplem14  12277  pythagtriplem16  12279  pceu  12295  pcfac  12348  prmpwdvds  12353  4sqlem5  12380  mul4sqlem  12391  ennnfonelem0  12406  ennnfonelemfun  12418  ennnfonelemf1  12419  ennnfonelemrn  12420  ctinfomlemom  12428  nninfdclemp1  12451  ndxid  12486  setsfun0  12498  setsresg  12500  setscom  12502  strslfv2d  12505  ressval3d  12531  resseqnbasd  12532  imasaddvallemg  12736  xpsval  12771  plusffvalg  12781  mgm1  12789  grpidvalg  12792  sgrp1  12816  mnd1  12847  mnd1id  12848  grppropstrg  12895  grpinvfvalg  12915  grpsubfvalg  12918  grp1  12976  mulgfvalg  12985  mulg2  12992  subsubg  13057  releqgg  13080  eqgfval  13081  mgpvalg  13133  mgpbasg  13136  mgpscag  13137  mgptopng  13139  mgpdsg  13140  mgpress  13141  ringidvalg  13144  ring1  13236  opprvalg  13241  opprmulfvalg  13242  opprbasg  13247  oppraddg  13248  subsubrg  13366  scaffvalg  13396  lmodpropd  13439  tgidm  13577  tgrest  13672  ssidcn  13713  txcnmpt  13776  txcn  13778  blres  13937  mopnval  13945  remetdval  14042  divccncfap  14080  cncfmet  14082  cncfcncntop  14083  cnplimcim  14139  cnplimclemr  14141  limccnpcntop  14147  limccnp2cntop  14149  dvexp  14178  sin0pilem1  14205  pilem3  14207  ef2kpi  14230  sin2pim  14237  cos2pim  14238  sinmpi  14239  cosmpi  14240  sinppi  14241  cosppi  14242  sinhalfpip  14244  sinhalfpim  14245  coshalfpip  14246  coshalfpim  14247  tangtx  14262  1cxp  14324  ecxp  14325  rplogb1  14369  rpelogb  14370  binom4  14400  lgslem1  14404  lgseisenlem1  14453  lgseisenlem2  14454  m1lgs  14455  2sqlem8  14473  ex-ceil  14481  qdencn  14778  cvgcmp2nlemabs  14783  trilpolemlt1  14792  nconstwlpolem0  14813