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  3799  intsng  3878  riinm  3959  iinxsng  3960  iunxprg  3967  rintm  3979  sucprc  4412  unisucg  4414  xpriindim  4765  relop  4777  dmxpm  4847  riinint  4888  resabs1  4936  resabs2  4938  resima2  4941  xpssres  4942  resopab2  4954  imasng  4993  ndmima  5005  xpdisj1  5053  xpdisj2  5054  djudisj  5056  resdisj  5057  rnxpm  5058  xpima1  5075  xpima2m  5076  dmsnsnsng  5106  rnsnopg  5107  rnpropg  5108  mptiniseg  5123  dfco2a  5129  relcoi1  5160  unixpm  5164  iotaval  5189  funtp  5269  fnun  5322  fnresdisj  5326  fnima  5334  fnimaeq0  5337  fcoi1  5396  f1orescnv  5477  foun  5480  resdif  5483  tz6.12-2  5506  fveu  5507  tz6.12-1  5542  fvun2  5583  fvopab3ig  5590  f1oresrab  5681  dfmptg  5695  ressnop0  5697  fvunsng  5710  fnsnsplitss  5715  fsnunfv  5717  fvpr1  5720  fvpr2  5721  fvpr1g  5722  fvpr2g  5723  fvtp1g  5724  fvtp2g  5725  fvtp3g  5726  fvtp2  5728  fvtp3  5729  f1oiso2  5827  riotaund  5864  ovprc  5909  resoprab2  5971  fnoprabg  5975  ovidig  5991  ovigg  5994  ov6g  6011  ovconst2  6025  offval2  6097  ot1stg  6152  ot2ndg  6153  ot3rdgg  6154  fmpoco  6216  algrflemg  6230  tpostpos2  6265  rdgisuc1  6384  frec0g  6397  frecsuclem  6406  frecrdg  6408  oasuc  6464  oa1suc  6467  omsuc  6472  nnm1  6525  nnm2  6526  dfec2  6537  errn  6556  ixpsnval  6700  ixpintm  6724  mapen  6845  xpmapenlem  6848  phplem2  6852  undifdc  6922  fisseneq  6930  ssfirab  6932  eqinfti  7018  infvalti  7020  infsnti  7028  casef  7086  caseinl  7089  caseinr  7090  djudom  7091  ctssdccl  7109  nninfwlpoimlemginf  7173  exmidfodomrlemim  7199  1qec  7386  mulidnq  7387  addpinq1  7462  suplocexprlem2b  7712  suplocexprlemlub  7722  0idsr  7765  1idsr  7766  caucvgsrlemoffres  7798  caucvgsr  7800  mulresr  7836  pitonnlem2  7845  ax1rid  7875  axcnre  7879  negid  8203  subneg  8205  negneg  8206  dfinfre  8912  2times  9046  infrenegsupex  9593  rexneg  9829  xaddpnf2  9846  xaddmnf1  9847  xaddmnf2  9848  fseq1p1m1  10093  fzosplitprm1  10233  intfracq  10319  frec2uz0d  10398  frec2uzrdg  10408  frecuzrdg0  10412  frecuzrdgg  10415  frecuzrdg0t  10421  seq3val  10457  seqvalcd  10458  iseqf1olemjpcl  10494  iseqf1olemqpcl  10495  iseqf1olemfvp  10496  seq3f1olemqsum  10499  sqval  10577  iexpcyc  10624  binom3  10637  faclbnd  10720  faclbnd2  10721  bcn1  10737  hashinfom  10757  hashennn  10759  hashxp  10805  shftlem  10824  shftuz  10825  shftidt  10841  reim0  10869  remullem  10879  resqrexlemf1  11016  resqrexlemcalc3  11024  absexpzap  11088  absimle  11092  amgm2  11126  minmax  11237  mingeb  11249  2zinfmin  11250  xrmaxiflemval  11257  xrmaxadd  11268  infxrnegsupex  11270  xrminmax  11272  summodc  11390  fsum3  11394  sumsnf  11416  sumsns  11422  isumclim3  11430  isumge0  11437  fsump1i  11440  fsum2dlemstep  11441  fisumcom2  11445  fsumshftm  11452  fsumconst  11461  fsumiun  11484  hashrabrex  11488  hashuni  11489  binom11  11493  isumsplit  11498  geo2sum  11521  mertensabs  11544  prodmodc  11585  fprodseq  11590  prodsnf  11599  prodsns  11610  fprodconst  11627  fprod2dlemstep  11629  fprodcom2fi  11633  efgt1p2  11702  efgt1p  11703  resinval  11722  recosval  11723  cosadd  11744  ef01bndlem  11763  eirraplem  11783  ialgr0  12043  algrp1  12045  eucalg  12058  phiprmpw  12221  phiprm  12222  prmdiv  12234  pythagtriplem12  12274  pythagtriplem14  12276  pythagtriplem16  12278  pceu  12294  pcfac  12347  prmpwdvds  12352  4sqlem5  12379  mul4sqlem  12390  ennnfonelem0  12405  ennnfonelemfun  12417  ennnfonelemf1  12418  ennnfonelemrn  12419  ctinfomlemom  12427  nninfdclemp1  12450  ndxid  12485  setsfun0  12497  setsresg  12499  setscom  12501  strslfv2d  12504  ressval3d  12530  resseqnbasd  12531  imasaddvallemg  12735  xpsval  12770  plusffvalg  12780  mgm1  12788  grpidvalg  12791  sgrp1  12815  mnd1  12846  mnd1id  12847  grppropstrg  12894  grpinvfvalg  12914  grpsubfvalg  12917  grp1  12975  mulgfvalg  12984  mulg2  12991  subsubg  13055  releqgg  13078  eqgfval  13079  mgpvalg  13131  mgpbasg  13134  mgpscag  13135  mgptopng  13137  mgpdsg  13138  mgpress  13139  ringidvalg  13142  ring1  13234  opprvalg  13239  opprmulfvalg  13240  opprbasg  13245  oppraddg  13246  subsubrg  13364  scaffvalg  13394  tgidm  13544  tgrest  13639  ssidcn  13680  txcnmpt  13743  txcn  13745  blres  13904  mopnval  13912  remetdval  14009  divccncfap  14047  cncfmet  14049  cncfcncntop  14050  cnplimcim  14106  cnplimclemr  14108  limccnpcntop  14114  limccnp2cntop  14116  dvexp  14145  sin0pilem1  14172  pilem3  14174  ef2kpi  14197  sin2pim  14204  cos2pim  14205  sinmpi  14206  cosmpi  14207  sinppi  14208  cosppi  14209  sinhalfpip  14211  sinhalfpim  14212  coshalfpip  14213  coshalfpim  14214  tangtx  14229  1cxp  14291  ecxp  14292  rplogb1  14336  rpelogb  14337  binom4  14367  lgslem1  14371  lgseisenlem1  14420  lgseisenlem2  14421  m1lgs  14422  2sqlem8  14440  ex-ceil  14448  qdencn  14745  cvgcmp2nlemabs  14750  trilpolemlt1  14759  nconstwlpolem0  14780