Theorem eqtrid 2215

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

Syntax hints:   -> wi 4   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  eqtr2id  2216  eqtr3id  2217  3eqtr3a  2227  3eqtr4g  2228  csbtt  3061  csbvarg  3077  csbie2g  3099  rabbi2dva  3335  csbprc  3460  disjssun  3478  disjpr2  3647  prprc2  3692  difprsn2  3720  opprc  3786  intsng  3865  riinm  3945  iinxsng  3946  iunxprg  3953  rintm  3965  sucprc  4397  unisucg  4399  xpriindim  4749  relop  4761  dmxpm  4831  riinint  4872  resabs1  4920  resabs2  4922  resima2  4925  xpssres  4926  resopab2  4938  imasng  4976  ndmima  4988  xpdisj1  5035  xpdisj2  5036  djudisj  5038  resdisj  5039  rnxpm  5040  xpima1  5057  xpima2m  5058  dmsnsnsng  5088  rnsnopg  5089  rnpropg  5090  mptiniseg  5105  dfco2a  5111  relcoi1  5142  unixpm  5146  iotaval  5171  funtp  5251  fnun  5304  fnresdisj  5308  fnima  5316  fnimaeq0  5319  fcoi1  5378  f1orescnv  5458  foun  5461  resdif  5464  tz6.12-2  5487  fveu  5488  tz6.12-1  5523  fvun2  5563  fvopab3ig  5570  f1oresrab  5661  dfmptg  5675  ressnop0  5677  fvunsng  5690  fnsnsplitss  5695  fsnunfv  5697  fvpr1  5700  fvpr2  5701  fvpr1g  5702  fvpr2g  5703  fvtp1g  5704  fvtp2g  5705  fvtp3g  5706  fvtp2  5708  fvtp3  5709  f1oiso2  5806  riotaund  5843  ovprc  5888  resoprab2  5950  fnoprabg  5954  ovidig  5970  ovigg  5973  ov6g  5990  ovconst2  6004  offval2  6076  ot1stg  6131  ot2ndg  6132  ot3rdgg  6133  fmpoco  6195  algrflemg  6209  tpostpos2  6244  rdgisuc1  6363  frec0g  6376  frecsuclem  6385  frecrdg  6387  oasuc  6443  oa1suc  6446  omsuc  6451  nnm1  6504  nnm2  6505  dfec2  6516  errn  6535  ixpsnval  6679  ixpintm  6703  mapen  6824  xpmapenlem  6827  phplem2  6831  undifdc  6901  fisseneq  6909  ssfirab  6911  eqinfti  6997  infvalti  6999  infsnti  7007  casef  7065  caseinl  7068  caseinr  7069  djudom  7070  ctssdccl  7088  nninfwlpoimlemginf  7152  exmidfodomrlemim  7178  1qec  7350  mulidnq  7351  addpinq1  7426  suplocexprlem2b  7676  suplocexprlemlub  7686  0idsr  7729  1idsr  7730  caucvgsrlemoffres  7762  caucvgsr  7764  mulresr  7800  pitonnlem2  7809  ax1rid  7839  axcnre  7843  negid  8166  subneg  8168  negneg  8169  dfinfre  8872  2times  9006  infrenegsupex  9553  rexneg  9787  xaddpnf2  9804  xaddmnf1  9805  xaddmnf2  9806  fseq1p1m1  10050  fzosplitprm1  10190  intfracq  10276  frec2uz0d  10355  frec2uzrdg  10365  frecuzrdg0  10369  frecuzrdgg  10372  frecuzrdg0t  10378  seq3val  10414  seqvalcd  10415  iseqf1olemjpcl  10451  iseqf1olemqpcl  10452  iseqf1olemfvp  10453  seq3f1olemqsum  10456  sqval  10534  iexpcyc  10580  binom3  10593  faclbnd  10675  faclbnd2  10676  bcn1  10692  hashinfom  10712  hashennn  10714  hashxp  10761  shftlem  10780  shftuz  10781  shftidt  10797  reim0  10825  remullem  10835  resqrexlemf1  10972  resqrexlemcalc3  10980  absexpzap  11044  absimle  11048  amgm2  11082  minmax  11193  mingeb  11205  2zinfmin  11206  xrmaxiflemval  11213  xrmaxadd  11224  infxrnegsupex  11226  xrminmax  11228  summodc  11346  fsum3  11350  sumsnf  11372  sumsns  11378  isumclim3  11386  isumge0  11393  fsump1i  11396  fsum2dlemstep  11397  fisumcom2  11401  fsumshftm  11408  fsumconst  11417  fsumiun  11440  hashrabrex  11444  hashuni  11445  binom11  11449  isumsplit  11454  geo2sum  11477  mertensabs  11500  prodmodc  11541  fprodseq  11546  prodsnf  11555  prodsns  11566  fprodconst  11583  fprod2dlemstep  11585  fprodcom2fi  11589  efgt1p2  11658  efgt1p  11659  resinval  11678  recosval  11679  cosadd  11700  ef01bndlem  11719  eirraplem  11739  ialgr0  11998  algrp1  12000  eucalg  12013  phiprmpw  12176  phiprm  12177  prmdiv  12189  pythagtriplem12  12229  pythagtriplem14  12231  pythagtriplem16  12233  pceu  12249  pcfac  12302  prmpwdvds  12307  4sqlem5  12334  mul4sqlem  12345  ennnfonelem0  12360  ennnfonelemfun  12372  ennnfonelemf1  12373  ennnfonelemrn  12374  ctinfomlemom  12382  nninfdclemp1  12405  ndxid  12440  setsfun0  12452  setsresg  12454  setscom  12456  strslfv2d  12458  ressid2  12477  ressval2  12478  plusffvalg  12616  mgm1  12624  grpidvalg  12627  sgrp1  12651  mnd1  12679  mnd1id  12680  grpinvfvalg  12745  grpsubfvalg  12748  tgidm  12868  tgrest  12963  ssidcn  13004  txcnmpt  13067  txcn  13069  blres  13228  mopnval  13236  remetdval  13333  divccncfap  13371  cncfmet  13373  cncfcncntop  13374  cnplimcim  13430  cnplimclemr  13432  limccnpcntop  13438  limccnp2cntop  13440  dvexp  13469  sin0pilem1  13496  pilem3  13498  ef2kpi  13521  sin2pim  13528  cos2pim  13529  sinmpi  13530  cosmpi  13531  sinppi  13532  cosppi  13533  sinhalfpip  13535  sinhalfpim  13536  coshalfpip  13537  coshalfpim  13538  tangtx  13553  1cxp  13615  ecxp  13616  rplogb1  13660  rpelogb  13661  binom4  13691  lgslem1  13695  2sqlem8  13753  ex-ceil  13761  qdencn  14059  cvgcmp2nlemabs  14064  trilpolemlt1  14073  nconstwlpolem0  14094