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  3069  csbvarg  3085  csbie2g  3107  rabbi2dva  3343  csbprc  3468  disjssun  3486  disjpr2  3656  prprc2  3701  difprsn2  3732  opprc  3798  intsng  3877  riinm  3957  iinxsng  3958  iunxprg  3965  rintm  3977  sucprc  4410  unisucg  4412  xpriindim  4762  relop  4774  dmxpm  4844  riinint  4885  resabs1  4933  resabs2  4935  resima2  4938  xpssres  4939  resopab2  4951  imasng  4990  ndmima  5002  xpdisj1  5050  xpdisj2  5051  djudisj  5053  resdisj  5054  rnxpm  5055  xpima1  5072  xpima2m  5073  dmsnsnsng  5103  rnsnopg  5104  rnpropg  5105  mptiniseg  5120  dfco2a  5126  relcoi1  5157  unixpm  5161  iotaval  5186  funtp  5266  fnun  5319  fnresdisj  5323  fnima  5331  fnimaeq0  5334  fcoi1  5393  f1orescnv  5474  foun  5477  resdif  5480  tz6.12-2  5503  fveu  5504  tz6.12-1  5539  fvun2  5580  fvopab3ig  5587  f1oresrab  5678  dfmptg  5692  ressnop0  5694  fvunsng  5707  fnsnsplitss  5712  fsnunfv  5714  fvpr1  5717  fvpr2  5718  fvpr1g  5719  fvpr2g  5720  fvtp1g  5721  fvtp2g  5722  fvtp3g  5723  fvtp2  5725  fvtp3  5726  f1oiso2  5823  riotaund  5860  ovprc  5905  resoprab2  5967  fnoprabg  5971  ovidig  5987  ovigg  5990  ov6g  6007  ovconst2  6021  offval2  6093  ot1stg  6148  ot2ndg  6149  ot3rdgg  6150  fmpoco  6212  algrflemg  6226  tpostpos2  6261  rdgisuc1  6380  frec0g  6393  frecsuclem  6402  frecrdg  6404  oasuc  6460  oa1suc  6463  omsuc  6468  nnm1  6521  nnm2  6522  dfec2  6533  errn  6552  ixpsnval  6696  ixpintm  6720  mapen  6841  xpmapenlem  6844  phplem2  6848  undifdc  6918  fisseneq  6926  ssfirab  6928  eqinfti  7014  infvalti  7016  infsnti  7024  casef  7082  caseinl  7085  caseinr  7086  djudom  7087  ctssdccl  7105  nninfwlpoimlemginf  7169  exmidfodomrlemim  7195  1qec  7382  mulidnq  7383  addpinq1  7458  suplocexprlem2b  7708  suplocexprlemlub  7718  0idsr  7761  1idsr  7762  caucvgsrlemoffres  7794  caucvgsr  7796  mulresr  7832  pitonnlem2  7841  ax1rid  7871  axcnre  7875  negid  8198  subneg  8200  negneg  8201  dfinfre  8907  2times  9041  infrenegsupex  9588  rexneg  9824  xaddpnf2  9841  xaddmnf1  9842  xaddmnf2  9843  fseq1p1m1  10087  fzosplitprm1  10227  intfracq  10313  frec2uz0d  10392  frec2uzrdg  10402  frecuzrdg0  10406  frecuzrdgg  10409  frecuzrdg0t  10415  seq3val  10451  seqvalcd  10452  iseqf1olemjpcl  10488  iseqf1olemqpcl  10489  iseqf1olemfvp  10490  seq3f1olemqsum  10493  sqval  10571  iexpcyc  10617  binom3  10630  faclbnd  10712  faclbnd2  10713  bcn1  10729  hashinfom  10749  hashennn  10751  hashxp  10797  shftlem  10816  shftuz  10817  shftidt  10833  reim0  10861  remullem  10871  resqrexlemf1  11008  resqrexlemcalc3  11016  absexpzap  11080  absimle  11084  amgm2  11118  minmax  11229  mingeb  11241  2zinfmin  11242  xrmaxiflemval  11249  xrmaxadd  11260  infxrnegsupex  11262  xrminmax  11264  summodc  11382  fsum3  11386  sumsnf  11408  sumsns  11414  isumclim3  11422  isumge0  11429  fsump1i  11432  fsum2dlemstep  11433  fisumcom2  11437  fsumshftm  11444  fsumconst  11453  fsumiun  11476  hashrabrex  11480  hashuni  11481  binom11  11485  isumsplit  11490  geo2sum  11513  mertensabs  11536  prodmodc  11577  fprodseq  11582  prodsnf  11591  prodsns  11602  fprodconst  11619  fprod2dlemstep  11621  fprodcom2fi  11625  efgt1p2  11694  efgt1p  11695  resinval  11714  recosval  11715  cosadd  11736  ef01bndlem  11755  eirraplem  11775  ialgr0  12034  algrp1  12036  eucalg  12049  phiprmpw  12212  phiprm  12213  prmdiv  12225  pythagtriplem12  12265  pythagtriplem14  12267  pythagtriplem16  12269  pceu  12285  pcfac  12338  prmpwdvds  12343  4sqlem5  12370  mul4sqlem  12381  ennnfonelem0  12396  ennnfonelemfun  12408  ennnfonelemf1  12409  ennnfonelemrn  12410  ctinfomlemom  12418  nninfdclemp1  12441  ndxid  12476  setsfun0  12488  setsresg  12490  setscom  12492  strslfv2d  12495  ressval3d  12521  resseqnbasd  12522  plusffvalg  12711  mgm1  12719  grpidvalg  12722  sgrp1  12746  mnd1  12775  mnd1id  12776  grppropstrg  12823  grpinvfvalg  12843  grpsubfvalg  12846  grp1  12904  mulgfvalg  12913  mulg2  12920  subsubg  12983  mgpvalg  13033  mgpbasg  13036  mgpscag  13037  mgptopng  13039  mgpdsg  13040  mgpress  13041  ringidvalg  13044  ring1  13136  opprvalg  13140  opprmulfvalg  13141  opprbasg  13146  oppraddg  13147  tgidm  13356  tgrest  13451  ssidcn  13492  txcnmpt  13555  txcn  13557  blres  13716  mopnval  13724  remetdval  13821  divccncfap  13859  cncfmet  13861  cncfcncntop  13862  cnplimcim  13918  cnplimclemr  13920  limccnpcntop  13926  limccnp2cntop  13928  dvexp  13957  sin0pilem1  13984  pilem3  13986  ef2kpi  14009  sin2pim  14016  cos2pim  14017  sinmpi  14018  cosmpi  14019  sinppi  14020  cosppi  14021  sinhalfpip  14023  sinhalfpim  14024  coshalfpip  14025  coshalfpim  14026  tangtx  14041  1cxp  14103  ecxp  14104  rplogb1  14148  rpelogb  14149  binom4  14179  lgslem1  14183  2sqlem8  14241  ex-ceil  14249  qdencn  14546  cvgcmp2nlemabs  14551  trilpolemlt1  14560  nconstwlpolem0  14581