Theorem eqtrid 2277

Description: An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)

Hypotheses

Ref	Expression
eqtrid.1	⊢ 𝐴 = 𝐵
eqtrid.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
eqtrid	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem eqtrid

Step	Hyp	Ref	Expression
1		eqtrid.1	. . 3 ⊢ 𝐴 = 𝐵
2	1	a1i 9	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		eqtrid.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	eqtrd 2265	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  eqtr2id  2278  eqtr3id  2279  3eqtr3a  2289  3eqtr4g  2290  eqab  2367  csbtt  3149  csbvarg  3165  csbie2g  3188  rabbi2dva  3428  csbprc  3553  disjssun  3571  disjpr2  3752  rabsnif  3757  prprc2  3800  difprsn2  3833  opprc  3903  intsng  3982  riinm  4063  iinxsng  4064  iunxprg  4071  rintm  4083  sucprc  4532  unisucg  4534  xpriindim  4892  relop  4904  dmxpm  4976  riinint  5017  resabs1  5066  resabs2  5068  resima2  5071  xpssres  5072  resopab2  5084  mptimass  5113  imasng  5126  ndmima  5138  xpdisj1  5186  xpdisj2  5187  djudisj  5189  resdisj  5190  rnxpm  5191  xpima1  5208  xpima2m  5209  dmsnsnsng  5239  rnsnopg  5240  rnpropg  5241  mptiniseg  5256  dfco2a  5262  relcoi1  5293  unixpm  5297  iotaval  5323  funtp  5408  fnun  5463  fnresdisj  5467  fnima  5476  fnimaeq0  5479  fresaunres2disj  5544  fcoi1  5546  f1orescnv  5629  foun  5632  resdif  5635  tz6.12-2  5660  fveu  5661  tz6.12-1  5696  fvun2  5743  fvopab3ig  5750  f1oresrab  5841  dfmptg  5856  funopsn  5859  ressnop0  5864  fvunsng  5877  fnsnsplitss  5882  fsnunfv  5884  fvpr1  5887  fvpr2  5888  fvpr1g  5889  fvpr2g  5890  fvtp1g  5891  fvtp2g  5892  fvtp3g  5893  fvtp2  5895  fvtp3  5896  f1oiso2  5999  riotaund  6039  ovprc  6085  resoprab2  6149  fnoprabg  6153  ovidig  6170  ovigg  6173  fvmpopr2d  6189  ov6g  6191  ovconst2  6205  offval2  6281  ot1stg  6345  ot2ndg  6346  ot3rdgg  6347  opabn1stprc  6388  fmpoco  6411  algrflemg  6425  suppsnopdc  6449  tpostpos2  6495  rdgisuc1  6614  frec0g  6627  frecsuclem  6636  frecrdg  6638  oasuc  6696  oa1suc  6699  omsuc  6704  nnm1  6757  nnm2  6758  dfec2  6769  errn  6788  ixpsnval  6935  ixpintm  6959  mapen  7098  xpmapenlem  7101  phplem2  7106  undifdc  7183  prfidceq  7187  fisseneq  7194  ssfirab  7196  eqinfti  7310  infvalti  7312  infsnti  7320  casef  7378  caseinl  7381  caseinr  7382  djudom  7383  ctssdccl  7401  nninfwlpoimlemginf  7466  exmidfodomrlemim  7503  1qec  7699  mulidnq  7700  addpinq1  7775  suplocexprlem2b  8025  suplocexprlemlub  8035  0idsr  8078  1idsr  8079  caucvgsrlemoffres  8111  caucvgsr  8113  mulresr  8149  pitonnlem2  8158  ax1rid  8188  axcnre  8192  negid  8516  subneg  8518  negneg  8519  dfinfre  9226  2times  9361  infrenegsupex  9922  rexneg  10159  xaddpnf2  10176  xaddmnf1  10177  xaddmnf2  10178  fseq1p1m1  10424  fzosplitprm1  10576  intfracq  10678  frec2uz0d  10757  frec2uzrdg  10767  frecuzrdg0  10771  frecuzrdgg  10774  frecuzrdg0t  10780  seq3val  10818  seqvalcd  10819  iseqf1olemjpcl  10866  iseqf1olemqpcl  10867  iseqf1olemfvp  10868  seq3f1olemqsum  10871  seqf1oglem2  10878  sqval  10955  iexpcyc  11002  binom3  11015  faclbnd  11099  faclbnd2  11100  bcn1  11116  hashinfom  11136  hashennn  11138  hashxp  11186  hashfibclem  11199  hashfibc  11200  hashtpgim  11210  hashtpglem  11211  hashtpg  11212  csbwrdg  11247  ccatlid  11287  s1val  11298  swrd00g  11334  pfxclz  11364  pfxccatpfx2  11422  cats1fvn  11449  cats1fvd  11451  cats1lend  11452  shftlem  11494  shftuz  11495  shftidt  11511  reim0  11539  remullem  11549  resqrexlemf1  11686  resqrexlemcalc3  11694  absexpzap  11758  absimle  11762  amgm2  11796  minmax  11908  mingeb  11920  2zinfmin  11921  xrmaxiflemval  11928  xrmaxadd  11939  infxrnegsupex  11941  xrminmax  11943  summodc  12062  fsum3  12066  sumsnf  12088  sumsns  12094  isumclim3  12102  isumge0  12109  fsump1i  12112  fsum2dlemstep  12113  fisumcom2  12117  fsumshftm  12124  fsumconst  12133  fsumiun  12156  hashrabrex  12160  hashuni  12161  binom11  12165  isumsplit  12170  geo2sum  12193  mertensabs  12216  prodmodc  12257  fprodseq  12262  prodsnf  12271  prodsns  12282  fprodconst  12299  fprod2dlemstep  12301  fprodcom2fi  12305  efgt1p2  12374  efgt1p  12375  resinval  12394  recosval  12395  cosadd  12416  ef01bndlem  12435  eirraplem  12456  bits0  12627  nninfctlemfo  12729  ialgr0  12734  algrp1  12736  eucalg  12749  phiprmpw  12912  phiprm  12913  prmdiv  12925  pythagtriplem12  12966  pythagtriplem14  12968  pythagtriplem16  12970  pceu  12986  pcfac  13041  prmpwdvds  13046  4sqlem5  13073  mul4sqlem  13084  ennnfonelem0  13145  ennnfonelemfun  13157  ennnfonelemf1  13158  ennnfonelemrn  13159  ctinfomlemom  13167  nninfdclemp1  13190  ndxid  13225  setsfun0  13237  setsresg  13239  setscom  13241  strslfv2d  13244  basm  13263  ressval3d  13274  resseqnbasd  13275  prdsval  13475  pwsval  13493  pwsplusgval  13497  pwsmulrval  13498  imasaddvallemg  13517  xpsval  13554  plusffvalg  13564  mgm1  13572  grpidvalg  13575  sgrp1  13613  prdsidlem  13649  mnd1  13657  mnd1id  13658  subsubm  13685  grppropstrg  13721  grpinvfvalg  13744  grpsubfvalg  13747  grp1  13808  prdsinvlem  13810  pwsinvg  13814  mulgfvalg  13827  mulgnn0gsum  13834  mulg2  13837  subsubg  13903  releqgg  13926  eqgfval  13928  conjsubg  13983  gsumfzconstf  14048  mgpvalg  14056  mgpbasg  14059  mgpscag  14060  mgptopng  14062  mgpdsg  14063  mgpress  14064  ringidvalg  14094  ring1  14192  opprvalg  14202  opprmulfvalg  14203  opprbasg  14208  oppraddg  14209  subsubrng  14348  subsubrg  14379  rrgval  14396  scaffvalg  14441  lmodpropd  14484  lsssetm  14491  lsslss  14516  lspfval  14523  sraring  14584  lidlvalg  14606  rspvalg  14607  lidlss  14611  islidlm  14614  lidl0cl  14618  lidlacl  14619  lidlnegcl  14620  lidl0  14624  lidl1  14625  rspcl  14626  rspssid  14627  rsp0  14628  rspssp  14629  2idlval  14637  2idlvalg  14638  crngridl  14665  rspsn  14669  zrhval  14752  zrhvalg  14753  zlmval  14762  zlmbasg  14764  zlmplusgg  14765  zlmmulrg  14766  znval  14771  znzrh2  14781  znf1o  14786  psrval  14801  mplvalcoe  14832  mpl0fi  14844  mplnegfi  14847  tgidm  14926  tgrest  15021  ssidcn  15062  txcnmpt  15125  txcn  15127  blres  15286  mopnval  15294  remetdval  15399  expcn  15421  divccncfap  15442  cncfmet  15444  cncfcncntop  15445  hovergt0  15502  cnplimcim  15519  cnplimclemr  15521  limccnpcntop  15527  limccnp2cntop  15529  dvexp  15563  dvmptid  15568  dvmptfsum  15577  elply2  15587  elplyd  15593  plyaddlem1  15599  plymullem1  15600  plycjlemc  15612  sin0pilem1  15633  pilem3  15635  ef2kpi  15658  sin2pim  15665  cos2pim  15666  sinmpi  15667  cosmpi  15668  sinppi  15669  cosppi  15670  sinhalfpip  15672  sinhalfpim  15673  coshalfpip  15674  coshalfpim  15675  tangtx  15690  1cxp  15752  ecxp  15753  rplogb1  15800  rpelogb  15801  binom4  15831  0sgm  15840  fsumdvdsmul  15846  1sgmprm  15849  1sgm2ppw  15850  lgslem1  15860  gausslemma2dlem4  15924  lgseisenlem1  15930  lgseisenlem2  15931  lgseisenlem3  15932  lgseisenlem4  15933  lgseisen  15934  lgsquadlem1  15937  lgsquadlem2  15938  lgsquadlem3  15939  lgsquad2lem1  15941  m1lgs  15945  2lgslem3a  15953  2lgslem3b  15954  2lgslem3c  15955  2lgslem3d  15956  2sqlem8  15983  opvtxov  16005  opiedgov  16008  structiedg0val  16022  edgov  16045  edg0iedg0g  16048  upgredg  16126  usgrf1oedg  16187  ushgredgedg  16208  ushgredgedgloop  16210  griedg0ssusgr  16233  subgrprop3  16244  0uhgrsubgr  16247  vtxdgfval  16270  vtxdfifiun  16279  vtxdumgrfival  16280  vtxd0nedgbfi  16281  1hevtxdg1en  16290  upgriswlkdc  16342  wlkres  16361  trlreslem  16371  clwwlkn2  16403  eupthvdres  16457  eupth2lem3fi  16458  ex-ceil  16481  depindlem1  16488  qdencn  16794  cvgcmp2nlemabs  16803  trilpolemlt1  16812  nconstwlpolem0  16835  gfsump1  16854  gfsumcl  16855