Theorem eqtrid 2241

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

Syntax hints:   -> wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  eqtr2id  2242  eqtr3id  2243  3eqtr3a  2253  3eqtr4g  2254  csbtt  3096  csbvarg  3112  csbie2g  3135  rabbi2dva  3371  csbprc  3496  disjssun  3514  disjpr2  3686  prprc2  3731  difprsn2  3762  opprc  3829  intsng  3908  riinm  3989  iinxsng  3990  iunxprg  3997  rintm  4009  sucprc  4447  unisucg  4449  xpriindim  4804  relop  4816  dmxpm  4886  riinint  4927  resabs1  4975  resabs2  4977  resima2  4980  xpssres  4981  resopab2  4993  mptimass  5022  imasng  5034  ndmima  5046  xpdisj1  5094  xpdisj2  5095  djudisj  5097  resdisj  5098  rnxpm  5099  xpima1  5116  xpima2m  5117  dmsnsnsng  5147  rnsnopg  5148  rnpropg  5149  mptiniseg  5164  dfco2a  5170  relcoi1  5201  unixpm  5205  iotaval  5230  funtp  5311  fnun  5364  fnresdisj  5368  fnima  5376  fnimaeq0  5379  fcoi1  5438  f1orescnv  5520  foun  5523  resdif  5526  tz6.12-2  5549  fveu  5550  tz6.12-1  5585  fvun2  5628  fvopab3ig  5635  f1oresrab  5727  dfmptg  5741  ressnop0  5743  fvunsng  5756  fnsnsplitss  5761  fsnunfv  5763  fvpr1  5766  fvpr2  5767  fvpr1g  5768  fvpr2g  5769  fvtp1g  5770  fvtp2g  5771  fvtp3g  5772  fvtp2  5774  fvtp3  5775  f1oiso2  5874  riotaund  5912  ovprc  5957  resoprab2  6019  fnoprabg  6023  ovidig  6040  ovigg  6043  fvmpopr2d  6059  ov6g  6061  ovconst2  6075  offval2  6151  ot1stg  6210  ot2ndg  6211  ot3rdgg  6212  fmpoco  6274  algrflemg  6288  tpostpos2  6323  rdgisuc1  6442  frec0g  6455  frecsuclem  6464  frecrdg  6466  oasuc  6522  oa1suc  6525  omsuc  6530  nnm1  6583  nnm2  6584  dfec2  6595  errn  6614  ixpsnval  6760  ixpintm  6784  mapen  6907  xpmapenlem  6910  phplem2  6914  undifdc  6985  prfidceq  6989  fisseneq  6995  ssfirab  6997  eqinfti  7086  infvalti  7088  infsnti  7096  casef  7154  caseinl  7157  caseinr  7158  djudom  7159  ctssdccl  7177  nninfwlpoimlemginf  7242  exmidfodomrlemim  7268  1qec  7455  mulidnq  7456  addpinq1  7531  suplocexprlem2b  7781  suplocexprlemlub  7791  0idsr  7834  1idsr  7835  caucvgsrlemoffres  7867  caucvgsr  7869  mulresr  7905  pitonnlem2  7914  ax1rid  7944  axcnre  7948  negid  8273  subneg  8275  negneg  8276  dfinfre  8983  2times  9118  infrenegsupex  9668  rexneg  9905  xaddpnf2  9922  xaddmnf1  9923  xaddmnf2  9924  fseq1p1m1  10169  fzosplitprm1  10310  intfracq  10412  frec2uz0d  10491  frec2uzrdg  10501  frecuzrdg0  10505  frecuzrdgg  10508  frecuzrdg0t  10514  seq3val  10552  seqvalcd  10553  iseqf1olemjpcl  10600  iseqf1olemqpcl  10601  iseqf1olemfvp  10602  seq3f1olemqsum  10605  seqf1oglem2  10612  sqval  10689  iexpcyc  10736  binom3  10749  faclbnd  10833  faclbnd2  10834  bcn1  10850  hashinfom  10870  hashennn  10872  hashxp  10918  csbwrdg  10964  shftlem  10981  shftuz  10982  shftidt  10998  reim0  11026  remullem  11036  resqrexlemf1  11173  resqrexlemcalc3  11181  absexpzap  11245  absimle  11249  amgm2  11283  minmax  11395  mingeb  11407  2zinfmin  11408  xrmaxiflemval  11415  xrmaxadd  11426  infxrnegsupex  11428  xrminmax  11430  summodc  11548  fsum3  11552  sumsnf  11574  sumsns  11580  isumclim3  11588  isumge0  11595  fsump1i  11598  fsum2dlemstep  11599  fisumcom2  11603  fsumshftm  11610  fsumconst  11619  fsumiun  11642  hashrabrex  11646  hashuni  11647  binom11  11651  isumsplit  11656  geo2sum  11679  mertensabs  11702  prodmodc  11743  fprodseq  11748  prodsnf  11757  prodsns  11768  fprodconst  11785  fprod2dlemstep  11787  fprodcom2fi  11791  efgt1p2  11860  efgt1p  11861  resinval  11880  recosval  11881  cosadd  11902  ef01bndlem  11921  eirraplem  11942  bits0  12112  nninfctlemfo  12207  ialgr0  12212  algrp1  12214  eucalg  12227  phiprmpw  12390  phiprm  12391  prmdiv  12403  pythagtriplem12  12444  pythagtriplem14  12446  pythagtriplem16  12448  pceu  12464  pcfac  12519  prmpwdvds  12524  4sqlem5  12551  mul4sqlem  12562  ennnfonelem0  12622  ennnfonelemfun  12634  ennnfonelemf1  12635  ennnfonelemrn  12636  ctinfomlemom  12644  nninfdclemp1  12667  ndxid  12702  setsfun0  12714  setsresg  12716  setscom  12718  strslfv2d  12721  basm  12739  ressval3d  12750  resseqnbasd  12751  imasaddvallemg  12958  xpsval  12995  plusffvalg  13005  mgm1  13013  grpidvalg  13016  sgrp1  13054  mnd1  13087  mnd1id  13088  subsubm  13115  grppropstrg  13151  grpinvfvalg  13174  grpsubfvalg  13177  grp1  13238  mulgfvalg  13251  mulgnn0gsum  13258  mulg2  13261  subsubg  13327  releqgg  13350  eqgfval  13352  conjsubg  13407  gsumfzconstf  13472  mgpvalg  13479  mgpbasg  13482  mgpscag  13483  mgptopng  13485  mgpdsg  13486  mgpress  13487  ringidvalg  13517  ring1  13615  opprvalg  13625  opprmulfvalg  13626  opprbasg  13631  oppraddg  13632  subsubrng  13770  subsubrg  13801  rrgval  13818  scaffvalg  13862  lmodpropd  13905  lsssetm  13912  lsslss  13937  lspfval  13944  sraring  14005  lidlvalg  14027  rspvalg  14028  lidlss  14032  islidlm  14035  lidl0cl  14039  lidlacl  14040  lidlnegcl  14041  lidl0  14045  lidl1  14046  rspcl  14047  rspssid  14048  rsp0  14049  rspssp  14050  2idlval  14058  2idlvalg  14059  crngridl  14086  rspsn  14090  zrhval  14173  zrhvalg  14174  zlmval  14183  zlmbasg  14185  zlmplusgg  14186  zlmmulrg  14187  znval  14192  znzrh2  14202  znf1o  14207  psrval  14220  tgidm  14310  tgrest  14405  ssidcn  14446  txcnmpt  14509  txcn  14511  blres  14670  mopnval  14678  remetdval  14783  expcn  14805  divccncfap  14826  cncfmet  14828  cncfcncntop  14829  hovergt0  14886  cnplimcim  14903  cnplimclemr  14905  limccnpcntop  14911  limccnp2cntop  14913  dvexp  14947  dvmptid  14952  dvmptfsum  14961  elply2  14971  elplyd  14977  plyaddlem1  14983  plymullem1  14984  plycjlemc  14996  sin0pilem1  15017  pilem3  15019  ef2kpi  15042  sin2pim  15049  cos2pim  15050  sinmpi  15051  cosmpi  15052  sinppi  15053  cosppi  15054  sinhalfpip  15056  sinhalfpim  15057  coshalfpip  15058  coshalfpim  15059  tangtx  15074  1cxp  15136  ecxp  15137  rplogb1  15184  rpelogb  15185  binom4  15215  0sgm  15221  fsumdvdsmul  15227  1sgmprm  15230  1sgm2ppw  15231  lgslem1  15241  gausslemma2dlem4  15305  lgseisenlem1  15311  lgseisenlem2  15312  lgseisenlem3  15313  lgseisenlem4  15314  lgseisen  15315  lgsquadlem1  15318  lgsquadlem2  15319  lgsquadlem3  15320  lgsquad2lem1  15322  m1lgs  15326  2lgslem3a  15334  2lgslem3b  15335  2lgslem3c  15336  2lgslem3d  15337  2sqlem8  15364  ex-ceil  15372  qdencn  15671  cvgcmp2nlemabs  15676  trilpolemlt1  15685  nconstwlpolem0  15707