Theorem eqtrid 2283

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqtr2id  2284  eqtr3id  2285  3eqtr3a  2295  3eqtr4g  2296  eqab  2373  csbtt  3159  csbvarg  3175  csbie2g  3198  rabbi2dva  3439  csbprc  3572  disjssun  3588  inssdif0im  3592  disjpr2  3773  rabsnif  3778  prprc2  3822  difprsn2  3855  opprc  3925  intsng  4004  riinm  4085  iinxsng  4086  iunxprg  4093  rintm  4105  sucprc  4557  unisucg  4559  xpriindim  4918  relop  4930  dmxpm  5002  riinint  5043  resabs1  5092  resabs2  5094  resima2  5097  xpssres  5098  resopab2  5110  mptimass  5139  imasng  5152  ndmima  5164  xpdisj1  5212  xpdisj2  5213  djudisj  5215  resdisj  5216  rnxpm  5217  xpima1  5234  xpima2m  5235  dmsnsnsng  5265  rnsnopg  5266  rnpropg  5267  mptiniseg  5282  dfco2a  5288  relcoi1  5319  unixpm  5323  iotaval  5349  funtp  5434  fnun  5489  fnresdisj  5493  fnima  5502  fnimaeq0  5505  fresaunres2disj  5570  fcoi1  5572  f1orescnv  5655  foun  5658  resdif  5661  tz6.12-2  5686  fveu  5687  tz6.12-1  5722  fvun2  5770  fvopab3ig  5779  f1oresrab  5873  dfmptg  5888  funopsn  5891  ressnop0  5896  fvunsng  5909  fnsnsplitss  5914  fsnunfv  5916  fvpr1  5919  fvpr2  5920  fvpr1g  5921  fvpr2g  5922  fvtp1g  5923  fvtp2g  5924  fvtp3g  5925  fvtp2  5927  fvtp3  5928  f1oiso2  6033  riotaund  6075  ovprc  6121  resoprab2  6185  fnoprabg  6189  ovidig  6206  ovigg  6209  fvmpopr2d  6225  ov6g  6227  ovconst2  6241  offval2  6318  ot1stg  6386  ot2ndg  6387  ot3rdgg  6388  opabn1stprc  6429  fmpoco  6452  algrflemg  6466  suppsnopdc  6490  tpostpos2  6536  rdgisuc1  6655  frec0g  6668  frecsuclem  6677  frecrdg  6679  oasuc  6737  oa1suc  6740  omsuc  6745  nnm1  6798  nnm2  6799  dfec2  6810  errn  6829  ixpsnval  6983  ixpintm  7007  mapen  7146  xpmapenlem  7149  phplem2  7154  undifdc  7231  prfidceq  7235  fisseneq  7242  ssfirab  7244  eqinfti  7360  infvalti  7362  infsnti  7370  casef  7428  caseinl  7431  caseinr  7432  djudom  7433  ctssdccl  7451  nninfwlpoimlemginf  7516  exmidfodomrlemim  7553  1qec  7755  mulidnq  7756  addpinq1  7831  suplocexprlem2b  8081  suplocexprlemlub  8091  0idsr  8134  1idsr  8135  caucvgsrlemoffres  8167  caucvgsr  8169  mulresr  8205  pitonnlem2  8214  ax1rid  8244  axcnre  8248  negid  8573  subneg  8575  negneg  8576  dfinfre  9286  2times  9432  infrenegsupex  9994  rexneg  10232  xaddpnf2  10249  xaddmnf1  10250  xaddmnf2  10251  fseq1p1m1  10501  fzosplitprm1  10653  infssfzcldc  10669  infssfzledc  10670  intfracq  10757  frec2uz0d  10836  frec2uzrdg  10846  frecuzrdg0  10850  frecuzrdgg  10853  frecuzrdg0t  10859  seq3val  10897  seqvalcd  10898  iseqf1olemjpcl  10945  iseqf1olemqpcl  10946  iseqf1olemfvp  10947  seq3f1olemqsum  10950  seqf1oglem2  10957  sqval  11034  iexpcyc  11081  binom3  11094  faclbnd  11179  faclbnd2  11180  bcn1  11196  hashinfom  11217  hashennn  11219  hashxp  11267  hashfibclem  11282  hashfibc  11283  hashf1lem1  11285  hashf1lem2  11286  hashtpgim  11297  hashtpglem  11298  hashtpg  11299  csbwrdg  11334  ccatlid  11374  s1val  11385  swrd00g  11421  pfxclz  11451  pfxccatpfx2  11509  cats1fvn  11536  cats1fvd  11538  cats1lend  11539  shftlem  11581  shftuz  11582  shftidt  11598  reim0  11626  remullem  11636  resqrexlemf1  11774  resqrexlemcalc3  11782  absexpzap  11846  absimle  11850  amgm2  11884  minmax  11996  mingeb  12008  2zinfmin  12009  xrmaxiflemval  12016  xrmaxadd  12027  infxrnegsupex  12029  xrminmax  12031  summodc  12150  fsum3  12154  sumsnf  12176  sumsns  12182  isumclim3  12190  isumge0  12197  fsump1i  12200  fsum2dlemstep  12201  fisumcom2  12205  fsumshftm  12212  fsumconst  12221  fsumiun  12244  hashrabrex  12248  hashuni  12249  binom11  12253  isumsplit  12258  geo2sum  12281  mertensabs  12304  prodmodc  12345  fprodseq  12350  prodsnf  12359  prodsns  12370  fprodconst  12387  fprod2dlemstep  12389  fprodcom2fi  12393  efgt1p2  12462  efgt1p  12463  resinval  12482  recosval  12483  cosadd  12504  ef01bndlem  12523  eirraplem  12544  bits0  12715  nninfctlemfo  12817  ialgr0  12822  algrp1  12824  eucalg  12837  phiprmpw  13000  phiprm  13001  prmdiv  13013  pythagtriplem12  13054  pythagtriplem14  13056  pythagtriplem16  13058  pceu  13074  pcfac  13129  prmpwdvds  13134  4sqlem5  13161  mul4sqlem  13172  ballotfilem4  13241  ballotfilem1c  13251  ballotfilemgun  13268  ennnfonelem0  13296  ennnfonelemfun  13308  ennnfonelemf1  13309  ennnfonelemrn  13310  ctinfomlemom  13318  nninfdclemp1  13341  ndxid  13376  setsfun0  13388  setsresg  13390  setscom  13392  strslfv2d  13395  basm  13414  ressval3d  13426  resseqnbasd  13427  imasaddvallemg  13636  plusffvalg  13682  mgm1  13690  grpidvalg  13693  sgrp1  13726  mnd1  13762  mnd1id  13763  subsubm  13790  grppropstrg  13824  grpinvfvalg  13847  grpsubfvalg  13850  grp1  13911  mulgfvalg  13924  mulgnn0gzsum  13931  mulg2  13934  subsubg  14000  releqgg  14023  eqgfval  14025  conjsubg  14080  gzsumconstf  14144  gsump1  14157  gsumclfi  14159  gsummptfidmadd  14161  gsumconstcmn  14166  prdsval  14173  prdsidlem  14193  prdsinvlem  14196  xpsval  14201  pwsval  14204  pwsplusgval  14208  pwsmulrval  14209  pwsinvg  14215  mgpvalg  14220  mgpbasg  14224  mgpscag  14226  mgptopng  14228  mgpdsg  14229  mgpress  14230  ringidvalg  14264  ring1  14364  opprvalg  14374  opprmulfvalg  14375  opprbasg  14380  oppraddg  14381  subsubrng  14522  subsubrg  14553  rrgval  14570  scaffvalg  14643  lmodpropd  14686  lsssetm  14693  lsslss  14718  lspfval  14725  sraring  14786  lidlvalg  14808  rspvalg  14809  lidlss  14813  islidlm  14816  lidl0cl  14820  lidlacl  14821  lidlnegcl  14822  lidl0  14826  lidl1  14827  rspcl  14828  rspssid  14829  rsp0  14830  rspssp  14831  2idlval  14839  2idlvalg  14840  crngridl  14867  rspsn  14871  zrhval  14952  zrhvalg  14953  zlmval  14962  zlmbasg  14964  zlmplusgg  14965  zlmmulrg  14966  znval  14971  znzrh2  14981  znf1o  14986  assapropd  15014  aspval  15015  psrval  15050  mplvalcoe  15081  mpl0fi  15093  mplnegfi  15096  tgidm  15175  tgrest  15270  ssidcn  15311  txcnmpt  15374  txcn  15376  blres  15535  mopnval  15543  remetdval  15648  expcn  15670  divccncfap  15691  cncfmet  15693  cncfcncntop  15694  hovergt0  15751  cnplimcim  15768  cnplimclemr  15770  limccnpcntop  15776  limccnp2cntop  15778  dvexp  15812  dvmptid  15817  dvmptfsum  15826  elply2  15836  elplyd  15842  plyaddlem1  15848  plymullem1  15849  plycjlemc  15861  sin0pilem1  15882  pilem3  15884  ef2kpi  15907  sin2pim  15914  cos2pim  15915  sinmpi  15916  cosmpi  15917  sinppi  15918  cosppi  15919  sinhalfpip  15921  sinhalfpim  15922  coshalfpip  15923  coshalfpim  15924  tangtx  15939  1cxp  16002  ecxp  16003  rplogb1  16050  rpelogb  16051  binom4  16081  log2tlbndlog2  16082  birthdaylem2  16088  birthdaylem3  16089  0sgm  16099  fsumdvdsmul  16105  1sgmprm  16108  1sgm2ppw  16109  lgslem1  16119  gausslemma2dlem4  16183  lgseisenlem1  16189  lgseisenlem2  16190  lgseisenlem3  16191  lgseisenlem4  16192  lgseisen  16193  lgsquadlem1  16196  lgsquadlem2  16197  lgsquadlem3  16198  lgsquad2lem1  16200  m1lgs  16204  2lgslem3a  16212  2lgslem3b  16213  2lgslem3c  16214  2lgslem3d  16215  2sqlem8  16242  opvtxov  16264  opiedgov  16267  structiedg0val  16281  edgov  16304  edg0iedg0g  16307  upgredg  16385  usgrf1oedg  16446  ushgredgedg  16467  ushgredgedgloop  16469  griedg0ssusgr  16492  subgrprop3  16503  0uhgrsubgr  16506  vtxdgfval  16529  vtxdfifiun  16538  vtxdumgrfival  16539  vtxd0nedgbfi  16540  1hevtxdg1en  16549  upgriswlkdc  16601  wlkres  16620  trlreslem  16630  clwwlkn2  16662  eupthvdres  16716  eupth2lem3fi  16717  ex-ceil  16740  depindlem1  16747  qdencn  17072  cvgcmp2nlemabs  17081  trilpolemlt1  17090  nconstwlpolem0  17113