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  3372  csbprc  3497  disjssun  3515  disjpr2  3687  prprc2  3732  difprsn2  3763  opprc  3830  intsng  3909  riinm  3990  iinxsng  3991  iunxprg  3998  rintm  4010  sucprc  4448  unisucg  4450  xpriindim  4805  relop  4817  dmxpm  4887  riinint  4928  resabs1  4976  resabs2  4978  resima2  4981  xpssres  4982  resopab2  4994  mptimass  5023  imasng  5035  ndmima  5047  xpdisj1  5095  xpdisj2  5096  djudisj  5098  resdisj  5099  rnxpm  5100  xpima1  5117  xpima2m  5118  dmsnsnsng  5148  rnsnopg  5149  rnpropg  5150  mptiniseg  5165  dfco2a  5171  relcoi1  5202  unixpm  5206  iotaval  5231  funtp  5312  fnun  5367  fnresdisj  5371  fnima  5379  fnimaeq0  5382  fcoi1  5441  f1orescnv  5523  foun  5526  resdif  5529  tz6.12-2  5552  fveu  5553  tz6.12-1  5588  fvun2  5631  fvopab3ig  5638  f1oresrab  5730  dfmptg  5744  ressnop0  5746  fvunsng  5759  fnsnsplitss  5764  fsnunfv  5766  fvpr1  5769  fvpr2  5770  fvpr1g  5771  fvpr2g  5772  fvtp1g  5773  fvtp2g  5774  fvtp3g  5775  fvtp2  5777  fvtp3  5778  f1oiso2  5877  riotaund  5915  ovprc  5961  resoprab2  6023  fnoprabg  6027  ovidig  6044  ovigg  6047  fvmpopr2d  6063  ov6g  6065  ovconst2  6079  offval2  6155  ot1stg  6219  ot2ndg  6220  ot3rdgg  6221  fmpoco  6283  algrflemg  6297  tpostpos2  6332  rdgisuc1  6451  frec0g  6464  frecsuclem  6473  frecrdg  6475  oasuc  6531  oa1suc  6534  omsuc  6539  nnm1  6592  nnm2  6593  dfec2  6604  errn  6623  ixpsnval  6769  ixpintm  6793  mapen  6916  xpmapenlem  6919  phplem2  6923  undifdc  6994  prfidceq  6998  fisseneq  7004  ssfirab  7006  eqinfti  7095  infvalti  7097  infsnti  7105  casef  7163  caseinl  7166  caseinr  7167  djudom  7168  ctssdccl  7186  nninfwlpoimlemginf  7251  exmidfodomrlemim  7280  1qec  7472  mulidnq  7473  addpinq1  7548  suplocexprlem2b  7798  suplocexprlemlub  7808  0idsr  7851  1idsr  7852  caucvgsrlemoffres  7884  caucvgsr  7886  mulresr  7922  pitonnlem2  7931  ax1rid  7961  axcnre  7965  negid  8290  subneg  8292  negneg  8293  dfinfre  9000  2times  9135  infrenegsupex  9685  rexneg  9922  xaddpnf2  9939  xaddmnf1  9940  xaddmnf2  9941  fseq1p1m1  10186  fzosplitprm1  10327  intfracq  10429  frec2uz0d  10508  frec2uzrdg  10518  frecuzrdg0  10522  frecuzrdgg  10525  frecuzrdg0t  10531  seq3val  10569  seqvalcd  10570  iseqf1olemjpcl  10617  iseqf1olemqpcl  10618  iseqf1olemfvp  10619  seq3f1olemqsum  10622  seqf1oglem2  10629  sqval  10706  iexpcyc  10753  binom3  10766  faclbnd  10850  faclbnd2  10851  bcn1  10867  hashinfom  10887  hashennn  10889  hashxp  10935  csbwrdg  10981  shftlem  10998  shftuz  10999  shftidt  11015  reim0  11043  remullem  11053  resqrexlemf1  11190  resqrexlemcalc3  11198  absexpzap  11262  absimle  11266  amgm2  11300  minmax  11412  mingeb  11424  2zinfmin  11425  xrmaxiflemval  11432  xrmaxadd  11443  infxrnegsupex  11445  xrminmax  11447  summodc  11565  fsum3  11569  sumsnf  11591  sumsns  11597  isumclim3  11605  isumge0  11612  fsump1i  11615  fsum2dlemstep  11616  fisumcom2  11620  fsumshftm  11627  fsumconst  11636  fsumiun  11659  hashrabrex  11663  hashuni  11664  binom11  11668  isumsplit  11673  geo2sum  11696  mertensabs  11719  prodmodc  11760  fprodseq  11765  prodsnf  11774  prodsns  11785  fprodconst  11802  fprod2dlemstep  11804  fprodcom2fi  11808  efgt1p2  11877  efgt1p  11878  resinval  11897  recosval  11898  cosadd  11919  ef01bndlem  11938  eirraplem  11959  bits0  12130  nninfctlemfo  12232  ialgr0  12237  algrp1  12239  eucalg  12252  phiprmpw  12415  phiprm  12416  prmdiv  12428  pythagtriplem12  12469  pythagtriplem14  12471  pythagtriplem16  12473  pceu  12489  pcfac  12544  prmpwdvds  12549  4sqlem5  12576  mul4sqlem  12587  ennnfonelem0  12647  ennnfonelemfun  12659  ennnfonelemf1  12660  ennnfonelemrn  12661  ctinfomlemom  12669  nninfdclemp1  12692  ndxid  12727  setsfun0  12739  setsresg  12741  setscom  12743  strslfv2d  12746  basm  12764  ressval3d  12775  resseqnbasd  12776  prdsval  12975  pwsval  12993  pwsplusgval  12997  pwsmulrval  12998  imasaddvallemg  13017  xpsval  13054  plusffvalg  13064  mgm1  13072  grpidvalg  13075  sgrp1  13113  prdsidlem  13149  mnd1  13157  mnd1id  13158  subsubm  13185  grppropstrg  13221  grpinvfvalg  13244  grpsubfvalg  13247  grp1  13308  prdsinvlem  13310  pwsinvg  13314  mulgfvalg  13327  mulgnn0gsum  13334  mulg2  13337  subsubg  13403  releqgg  13426  eqgfval  13428  conjsubg  13483  gsumfzconstf  13548  mgpvalg  13555  mgpbasg  13558  mgpscag  13559  mgptopng  13561  mgpdsg  13562  mgpress  13563  ringidvalg  13593  ring1  13691  opprvalg  13701  opprmulfvalg  13702  opprbasg  13707  oppraddg  13708  subsubrng  13846  subsubrg  13877  rrgval  13894  scaffvalg  13938  lmodpropd  13981  lsssetm  13988  lsslss  14013  lspfval  14020  sraring  14081  lidlvalg  14103  rspvalg  14104  lidlss  14108  islidlm  14111  lidl0cl  14115  lidlacl  14116  lidlnegcl  14117  lidl0  14121  lidl1  14122  rspcl  14123  rspssid  14124  rsp0  14125  rspssp  14126  2idlval  14134  2idlvalg  14135  crngridl  14162  rspsn  14166  zrhval  14249  zrhvalg  14250  zlmval  14259  zlmbasg  14261  zlmplusgg  14262  zlmmulrg  14263  znval  14268  znzrh2  14278  znf1o  14283  psrval  14296  tgidm  14394  tgrest  14489  ssidcn  14530  txcnmpt  14593  txcn  14595  blres  14754  mopnval  14762  remetdval  14867  expcn  14889  divccncfap  14910  cncfmet  14912  cncfcncntop  14913  hovergt0  14970  cnplimcim  14987  cnplimclemr  14989  limccnpcntop  14995  limccnp2cntop  14997  dvexp  15031  dvmptid  15036  dvmptfsum  15045  elply2  15055  elplyd  15061  plyaddlem1  15067  plymullem1  15068  plycjlemc  15080  sin0pilem1  15101  pilem3  15103  ef2kpi  15126  sin2pim  15133  cos2pim  15134  sinmpi  15135  cosmpi  15136  sinppi  15137  cosppi  15138  sinhalfpip  15140  sinhalfpim  15141  coshalfpip  15142  coshalfpim  15143  tangtx  15158  1cxp  15220  ecxp  15221  rplogb1  15268  rpelogb  15269  binom4  15299  0sgm  15305  fsumdvdsmul  15311  1sgmprm  15314  1sgm2ppw  15315  lgslem1  15325  gausslemma2dlem4  15389  lgseisenlem1  15395  lgseisenlem2  15396  lgseisenlem3  15397  lgseisenlem4  15398  lgseisen  15399  lgsquadlem1  15402  lgsquadlem2  15403  lgsquadlem3  15404  lgsquad2lem1  15406  m1lgs  15410  2lgslem3a  15418  2lgslem3b  15419  2lgslem3c  15420  2lgslem3d  15421  2sqlem8  15448  ex-ceil  15456  qdencn  15758  cvgcmp2nlemabs  15763  trilpolemlt1  15772  nconstwlpolem0  15794