Theorem eqtrid 2276

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 2264	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  eqtr2id  2277  eqtr3id  2278  3eqtr3a  2288  3eqtr4g  2289  csbtt  3139  csbvarg  3155  csbie2g  3178  rabbi2dva  3415  csbprc  3540  disjssun  3558  disjpr2  3733  rabsnif  3738  prprc2  3781  difprsn2  3813  opprc  3883  intsng  3962  riinm  4043  iinxsng  4044  iunxprg  4051  rintm  4063  sucprc  4509  unisucg  4511  xpriindim  4868  relop  4880  dmxpm  4952  riinint  4993  resabs1  5042  resabs2  5044  resima2  5047  xpssres  5048  resopab2  5060  mptimass  5089  imasng  5101  ndmima  5113  xpdisj1  5161  xpdisj2  5162  djudisj  5164  resdisj  5165  rnxpm  5166  xpima1  5183  xpima2m  5184  dmsnsnsng  5214  rnsnopg  5215  rnpropg  5216  mptiniseg  5231  dfco2a  5237  relcoi1  5268  unixpm  5272  iotaval  5298  funtp  5383  fnun  5438  fnresdisj  5442  fnima  5451  fnimaeq0  5454  fcoi1  5517  f1orescnv  5599  foun  5602  resdif  5605  tz6.12-2  5630  fveu  5631  tz6.12-1  5666  fvun2  5713  fvopab3ig  5720  f1oresrab  5812  dfmptg  5827  funopsn  5830  ressnop0  5835  fvunsng  5848  fnsnsplitss  5853  fsnunfv  5855  fvpr1  5858  fvpr2  5859  fvpr1g  5860  fvpr2g  5861  fvtp1g  5862  fvtp2g  5863  fvtp3g  5864  fvtp2  5866  fvtp3  5867  f1oiso2  5968  riotaund  6008  ovprc  6054  resoprab2  6118  fnoprabg  6122  ovidig  6139  ovigg  6142  fvmpopr2d  6158  ov6g  6160  ovconst2  6174  offval2  6251  ot1stg  6315  ot2ndg  6316  ot3rdgg  6317  opabn1stprc  6358  fmpoco  6381  algrflemg  6395  tpostpos2  6431  rdgisuc1  6550  frec0g  6563  frecsuclem  6572  frecrdg  6574  oasuc  6632  oa1suc  6635  omsuc  6640  nnm1  6693  nnm2  6694  dfec2  6705  errn  6724  ixpsnval  6870  ixpintm  6894  mapen  7032  xpmapenlem  7035  phplem2  7039  undifdc  7116  prfidceq  7120  fisseneq  7127  ssfirab  7129  eqinfti  7219  infvalti  7221  infsnti  7229  casef  7287  caseinl  7290  caseinr  7291  djudom  7292  ctssdccl  7310  nninfwlpoimlemginf  7375  exmidfodomrlemim  7412  1qec  7608  mulidnq  7609  addpinq1  7684  suplocexprlem2b  7934  suplocexprlemlub  7944  0idsr  7987  1idsr  7988  caucvgsrlemoffres  8020  caucvgsr  8022  mulresr  8058  pitonnlem2  8067  ax1rid  8097  axcnre  8101  negid  8426  subneg  8428  negneg  8429  dfinfre  9136  2times  9271  infrenegsupex  9828  rexneg  10065  xaddpnf2  10082  xaddmnf1  10083  xaddmnf2  10084  fseq1p1m1  10329  fzosplitprm1  10480  intfracq  10582  frec2uz0d  10661  frec2uzrdg  10671  frecuzrdg0  10675  frecuzrdgg  10678  frecuzrdg0t  10684  seq3val  10722  seqvalcd  10723  iseqf1olemjpcl  10770  iseqf1olemqpcl  10771  iseqf1olemfvp  10772  seq3f1olemqsum  10775  seqf1oglem2  10782  sqval  10859  iexpcyc  10906  binom3  10919  faclbnd  11003  faclbnd2  11004  bcn1  11020  hashinfom  11040  hashennn  11042  hashxp  11090  csbwrdg  11143  ccatlid  11183  s1val  11194  swrd00g  11230  pfxclz  11260  pfxccatpfx2  11318  cats1fvn  11345  cats1fvd  11347  cats1lend  11348  shftlem  11377  shftuz  11378  shftidt  11394  reim0  11422  remullem  11432  resqrexlemf1  11569  resqrexlemcalc3  11577  absexpzap  11641  absimle  11645  amgm2  11679  minmax  11791  mingeb  11803  2zinfmin  11804  xrmaxiflemval  11811  xrmaxadd  11822  infxrnegsupex  11824  xrminmax  11826  summodc  11945  fsum3  11949  sumsnf  11971  sumsns  11977  isumclim3  11985  isumge0  11992  fsump1i  11995  fsum2dlemstep  11996  fisumcom2  12000  fsumshftm  12007  fsumconst  12016  fsumiun  12039  hashrabrex  12043  hashuni  12044  binom11  12048  isumsplit  12053  geo2sum  12076  mertensabs  12099  prodmodc  12140  fprodseq  12145  prodsnf  12154  prodsns  12165  fprodconst  12182  fprod2dlemstep  12184  fprodcom2fi  12188  efgt1p2  12257  efgt1p  12258  resinval  12277  recosval  12278  cosadd  12299  ef01bndlem  12318  eirraplem  12339  bits0  12510  nninfctlemfo  12612  ialgr0  12617  algrp1  12619  eucalg  12632  phiprmpw  12795  phiprm  12796  prmdiv  12808  pythagtriplem12  12849  pythagtriplem14  12851  pythagtriplem16  12853  pceu  12869  pcfac  12924  prmpwdvds  12929  4sqlem5  12956  mul4sqlem  12967  ennnfonelem0  13027  ennnfonelemfun  13039  ennnfonelemf1  13040  ennnfonelemrn  13041  ctinfomlemom  13049  nninfdclemp1  13072  ndxid  13107  setsfun0  13119  setsresg  13121  setscom  13123  strslfv2d  13126  basm  13145  ressval3d  13156  resseqnbasd  13157  prdsval  13357  pwsval  13375  pwsplusgval  13379  pwsmulrval  13380  imasaddvallemg  13399  xpsval  13436  plusffvalg  13446  mgm1  13454  grpidvalg  13457  sgrp1  13495  prdsidlem  13531  mnd1  13539  mnd1id  13540  subsubm  13567  grppropstrg  13603  grpinvfvalg  13626  grpsubfvalg  13629  grp1  13690  prdsinvlem  13692  pwsinvg  13696  mulgfvalg  13709  mulgnn0gsum  13716  mulg2  13719  subsubg  13785  releqgg  13808  eqgfval  13810  conjsubg  13865  gsumfzconstf  13930  mgpvalg  13938  mgpbasg  13941  mgpscag  13942  mgptopng  13944  mgpdsg  13945  mgpress  13946  ringidvalg  13976  ring1  14074  opprvalg  14084  opprmulfvalg  14085  opprbasg  14090  oppraddg  14091  subsubrng  14230  subsubrg  14261  rrgval  14278  scaffvalg  14322  lmodpropd  14365  lsssetm  14372  lsslss  14397  lspfval  14404  sraring  14465  lidlvalg  14487  rspvalg  14488  lidlss  14492  islidlm  14495  lidl0cl  14499  lidlacl  14500  lidlnegcl  14501  lidl0  14505  lidl1  14506  rspcl  14507  rspssid  14508  rsp0  14509  rspssp  14510  2idlval  14518  2idlvalg  14519  crngridl  14546  rspsn  14550  zrhval  14633  zrhvalg  14634  zlmval  14643  zlmbasg  14645  zlmplusgg  14646  zlmmulrg  14647  znval  14652  znzrh2  14662  znf1o  14667  psrval  14682  mplvalcoe  14706  mpl0fi  14718  mplnegfi  14721  tgidm  14800  tgrest  14895  ssidcn  14936  txcnmpt  14999  txcn  15001  blres  15160  mopnval  15168  remetdval  15273  expcn  15295  divccncfap  15316  cncfmet  15318  cncfcncntop  15319  hovergt0  15376  cnplimcim  15393  cnplimclemr  15395  limccnpcntop  15401  limccnp2cntop  15403  dvexp  15437  dvmptid  15442  dvmptfsum  15451  elply2  15461  elplyd  15467  plyaddlem1  15473  plymullem1  15474  plycjlemc  15486  sin0pilem1  15507  pilem3  15509  ef2kpi  15532  sin2pim  15539  cos2pim  15540  sinmpi  15541  cosmpi  15542  sinppi  15543  cosppi  15544  sinhalfpip  15546  sinhalfpim  15547  coshalfpip  15548  coshalfpim  15549  tangtx  15564  1cxp  15626  ecxp  15627  rplogb1  15674  rpelogb  15675  binom4  15705  0sgm  15711  fsumdvdsmul  15717  1sgmprm  15720  1sgm2ppw  15721  lgslem1  15731  gausslemma2dlem4  15795  lgseisenlem1  15801  lgseisenlem2  15802  lgseisenlem3  15803  lgseisenlem4  15804  lgseisen  15805  lgsquadlem1  15808  lgsquadlem2  15809  lgsquadlem3  15810  lgsquad2lem1  15812  m1lgs  15816  2lgslem3a  15824  2lgslem3b  15825  2lgslem3c  15826  2lgslem3d  15827  2sqlem8  15854  opvtxov  15876  opiedgov  15879  structiedg0val  15893  edgov  15916  edg0iedg0g  15919  upgredg  15997  usgrf1oedg  16058  ushgredgedg  16079  ushgredgedgloop  16081  griedg0ssusgr  16104  subgrprop3  16115  0uhgrsubgr  16118  vtxdgfval  16141  vtxdfifiun  16150  vtxdumgrfival  16151  vtxd0nedgbfi  16152  1hevtxdg1en  16161  upgriswlkdc  16213  wlkres  16232  trlreslem  16242  clwwlkn2  16274  ex-ceil  16325  qdencn  16634  cvgcmp2nlemabs  16639  trilpolemlt1  16648  nconstwlpolem0  16670  gfsump1  16689  gfsumcl  16690