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  8574  subneg  8576  negneg  8577  dfinfre  9288  2times  9434  infrenegsupex  10003  rexneg  10242  xaddpnf2  10259  xaddmnf1  10260  xaddmnf2  10261  fseq1p1m1  10511  fzosplitprm1  10663  infssfzcldc  10679  infssfzledc  10680  intfracq  10770  frec2uz0d  10849  frec2uzrdg  10859  frecuzrdg0  10863  frecuzrdgg  10866  frecuzrdg0t  10872  seq3val  10910  seqvalcd  10911  iseqf1olemjpcl  10958  iseqf1olemqpcl  10959  iseqf1olemfvp  10960  seq3f1olemqsum  10963  seqf1oglem2  10970  sqval  11047  iexpcyc  11094  binom3  11107  faclbnd  11193  faclbnd2  11194  bcn1  11210  hashinfom  11231  hashennn  11233  hashxp  11281  hashfibclem  11296  hashfibc  11297  hashf1lem1  11299  hashf1lem2  11300  hashtpgim  11311  hashtpglem  11312  hashtpg  11313  csbwrdg  11348  ccatlid  11388  s1val  11399  swrd00g  11435  pfxclz  11465  pfxccatpfx2  11523  cats1fvn  11550  cats1fvd  11552  cats1lend  11553  shftlem  11595  shftuz  11596  shftidt  11612  reim0  11640  remullem  11650  resqrexlemf1  11788  resqrexlemcalc3  11796  absexpzap  11861  absimle  11865  amgm2  11899  minmax  12011  mingeb  12024  2zinfmin  12025  xrmaxiflemval  12032  xrmaxadd  12043  infxrnegsupex  12045  xrminmax  12047  summodc  12166  fsum3  12170  sumsnf  12192  sumsns  12198  isumclim3  12206  isumge0  12213  fsump1i  12216  fsum2dlemstep  12217  fisumcom2  12221  fsumshftm  12228  fsumconst  12237  fsumiun  12260  hashrabrex  12264  hashuni  12265  binom11  12269  isumsplit  12274  geo2sum  12297  mertensabs  12320  prodmodc  12361  fprodseq  12366  prodsnf  12375  prodsns  12386  fprodconst  12403  fprod2dlemstep  12405  fprodcom2fi  12409  efgt1p2  12478  efgt1p  12479  resinval  12498  recosval  12499  cosadd  12520  ef01bndlem  12539  eirraplem  12560  bits0  12731  nninfctlemfo  12833  ialgr0  12838  algrp1  12840  eucalg  12853  phiprmpw  13020  phiprm  13021  prmdiv  13033  pythagtriplem12  13074  pythagtriplem14  13076  pythagtriplem16  13078  pceu  13094  pcfac  13149  prmpwdvds  13154  4sqlem5  13181  mul4sqlem  13192  ballotfilem4  13290  ballotfilem1c  13300  ballotfilemgun  13317  ennnfonelem0  13345  ennnfonelemfun  13357  ennnfonelemf1  13358  ennnfonelemrn  13359  ctinfomlemom  13367  nninfdclemp1  13390  ndxid  13425  setsfun0  13437  setsresg  13439  setscom  13441  strslfv2d  13444  basm  13463  ressval3d  13475  resseqnbasd  13476  imasaddvallemg  13685  plusffvalg  13731  mgm1  13739  grpidvalg  13742  sgrp1  13775  mnd1  13811  mnd1id  13812  subsubm  13839  grppropstrg  13873  grpinvfvalg  13896  grpsubfvalg  13899  grp1  13960  mulgfvalg  13973  mulgnn0gzsum  13980  mulg2  13983  subsubg  14049  releqgg  14072  eqgfval  14074  conjsubg  14129  gzsumconstf  14193  gsump1  14206  gsumclfi  14208  gsummptfidmadd  14210  gsumconstcmn  14215  prdsval  14222  prdsidlem  14242  prdsinvlem  14245  xpsval  14250  pwsval  14253  pwsplusgval  14257  pwsmulrval  14258  pwsinvg  14264  mgpvalg  14269  mgpbasg  14273  mgpscag  14275  mgptopng  14277  mgpdsg  14278  mgpress  14279  ringidvalg  14313  ring1  14413  opprvalg  14423  opprmulfvalg  14424  opprbasg  14429  oppraddg  14430  subsubrng  14571  subsubrg  14602  rrgval  14619  scaffvalg  14692  lmodpropd  14735  lsssetm  14742  lsslss  14767  lspfval  14774  sraring  14835  lidlvalg  14857  rspvalg  14858  lidlss  14862  islidlm  14865  lidl0cl  14869  lidlacl  14870  lidlnegcl  14871  lidl0  14875  lidl1  14876  rspcl  14877  rspssid  14878  rsp0  14879  rspssp  14880  2idlval  14888  2idlvalg  14889  crngridl  14916  rspsn  14920  zrhval  15001  zrhvalg  15002  zlmval  15011  zlmbasg  15013  zlmplusgg  15014  zlmmulrg  15015  znval  15020  znzrh2  15030  znf1o  15035  assapropd  15063  aspval  15064  psrval  15099  mplvalcoe  15130  mpl0fi  15142  mplnegfi  15145  tgidm  15224  tgrest  15319  ssidcn  15360  txcnmpt  15423  txcn  15425  blres  15584  mopnval  15592  remetdval  15697  expcn  15719  divccncfap  15740  cncfmet  15742  cncfcncntop  15743  hovergt0  15800  cnplimcim  15817  cnplimclemr  15819  limccnpcntop  15825  limccnp2cntop  15827  dvexp  15861  dvmptid  15866  dvmptfsum  15875  elply2  15885  elplyd  15891  plyaddlem1  15897  plymullem1  15898  plycjlemc  15910  sin0pilem1  15932  pilem3  15934  ef2kpi  15957  sin2pim  15964  cos2pim  15965  sinmpi  15966  cosmpi  15967  sinppi  15968  cosppi  15969  sinhalfpip  15971  sinhalfpim  15972  coshalfpip  15973  coshalfpim  15974  tangtx  15989  1cxp  16055  ecxp  16056  rplogb1  16103  rpelogb  16104  zprmlogbaplem2  16135  binom4  16138  log2tlbndlog2  16139  birthdaylem2  16145  birthdaylem3  16146  0sgm  16166  fsumdvdsmul  16186  1sgmprm  16189  1sgm2ppw  16190  ppiqub  16194  lgslem1  16217  gausslemma2dlem4  16281  lgseisenlem1  16287  lgseisenlem2  16288  lgseisenlem3  16289  lgseisenlem4  16290  lgseisen  16291  lgsquadlem1  16294  lgsquadlem2  16295  lgsquadlem3  16296  lgsquad2lem1  16298  m1lgs  16302  2lgslem3a  16310  2lgslem3b  16311  2lgslem3c  16312  2lgslem3d  16313  2sqlem8  16340  opvtxov  16362  opiedgov  16365  structiedg0val  16379  edgov  16402  edg0iedg0g  16405  upgredg  16483  usgrf1oedg  16544  ushgredgedg  16565  ushgredgedgloop  16567  griedg0ssusgr  16590  subgrprop3  16601  0uhgrsubgr  16604  vtxdgfval  16627  vtxdfifiun  16636  vtxdumgrfival  16637  vtxd0nedgbfi  16638  1hevtxdg1en  16647  upgriswlkdc  16699  wlkres  16718  trlreslem  16728  clwwlkn2  16760  eupthvdres  16814  eupth2lem3fi  16815  ex-ceil  16838  depindlem1  16845  qdencn  17170  cvgcmp2nlemabs  17179  trilpolemlt1  17188  nconstwlpolem0  17211