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  5600  foun  5603  resdif  5606  tz6.12-2  5631  fveu  5632  tz6.12-1  5667  fvun2  5714  fvopab3ig  5721  f1oresrab  5813  dfmptg  5828  funopsn  5831  ressnop0  5836  fvunsng  5849  fnsnsplitss  5854  fsnunfv  5856  fvpr1  5859  fvpr2  5860  fvpr1g  5861  fvpr2g  5862  fvtp1g  5863  fvtp2g  5864  fvtp3g  5865  fvtp2  5867  fvtp3  5868  f1oiso2  5971  riotaund  6011  ovprc  6057  resoprab2  6121  fnoprabg  6125  ovidig  6142  ovigg  6145  fvmpopr2d  6161  ov6g  6163  ovconst2  6177  offval2  6254  ot1stg  6318  ot2ndg  6319  ot3rdgg  6320  opabn1stprc  6361  fmpoco  6384  algrflemg  6398  tpostpos2  6434  rdgisuc1  6553  frec0g  6566  frecsuclem  6575  frecrdg  6577  oasuc  6635  oa1suc  6638  omsuc  6643  nnm1  6696  nnm2  6697  dfec2  6708  errn  6727  ixpsnval  6873  ixpintm  6897  mapen  7035  xpmapenlem  7038  phplem2  7042  undifdc  7119  prfidceq  7123  fisseneq  7130  ssfirab  7132  eqinfti  7222  infvalti  7224  infsnti  7232  casef  7290  caseinl  7293  caseinr  7294  djudom  7295  ctssdccl  7313  nninfwlpoimlemginf  7378  exmidfodomrlemim  7415  1qec  7611  mulidnq  7612  addpinq1  7687  suplocexprlem2b  7937  suplocexprlemlub  7947  0idsr  7990  1idsr  7991  caucvgsrlemoffres  8023  caucvgsr  8025  mulresr  8061  pitonnlem2  8070  ax1rid  8100  axcnre  8104  negid  8429  subneg  8431  negneg  8432  dfinfre  9139  2times  9274  infrenegsupex  9831  rexneg  10068  xaddpnf2  10085  xaddmnf1  10086  xaddmnf2  10087  fseq1p1m1  10332  fzosplitprm1  10484  intfracq  10586  frec2uz0d  10665  frec2uzrdg  10675  frecuzrdg0  10679  frecuzrdgg  10682  frecuzrdg0t  10688  seq3val  10726  seqvalcd  10727  iseqf1olemjpcl  10774  iseqf1olemqpcl  10775  iseqf1olemfvp  10776  seq3f1olemqsum  10779  seqf1oglem2  10786  sqval  10863  iexpcyc  10910  binom3  10923  faclbnd  11007  faclbnd2  11008  bcn1  11024  hashinfom  11044  hashennn  11046  hashxp  11094  hashtpgim  11113  hashtpglem  11114  hashtpg  11115  csbwrdg  11150  ccatlid  11190  s1val  11201  swrd00g  11237  pfxclz  11267  pfxccatpfx2  11325  cats1fvn  11352  cats1fvd  11354  cats1lend  11355  shftlem  11397  shftuz  11398  shftidt  11414  reim0  11442  remullem  11452  resqrexlemf1  11589  resqrexlemcalc3  11597  absexpzap  11661  absimle  11665  amgm2  11699  minmax  11811  mingeb  11823  2zinfmin  11824  xrmaxiflemval  11831  xrmaxadd  11842  infxrnegsupex  11844  xrminmax  11846  summodc  11965  fsum3  11969  sumsnf  11991  sumsns  11997  isumclim3  12005  isumge0  12012  fsump1i  12015  fsum2dlemstep  12016  fisumcom2  12020  fsumshftm  12027  fsumconst  12036  fsumiun  12059  hashrabrex  12063  hashuni  12064  binom11  12068  isumsplit  12073  geo2sum  12096  mertensabs  12119  prodmodc  12160  fprodseq  12165  prodsnf  12174  prodsns  12185  fprodconst  12202  fprod2dlemstep  12204  fprodcom2fi  12208  efgt1p2  12277  efgt1p  12278  resinval  12297  recosval  12298  cosadd  12319  ef01bndlem  12338  eirraplem  12359  bits0  12530  nninfctlemfo  12632  ialgr0  12637  algrp1  12639  eucalg  12652  phiprmpw  12815  phiprm  12816  prmdiv  12828  pythagtriplem12  12869  pythagtriplem14  12871  pythagtriplem16  12873  pceu  12889  pcfac  12944  prmpwdvds  12949  4sqlem5  12976  mul4sqlem  12987  ennnfonelem0  13047  ennnfonelemfun  13059  ennnfonelemf1  13060  ennnfonelemrn  13061  ctinfomlemom  13069  nninfdclemp1  13092  ndxid  13127  setsfun0  13139  setsresg  13141  setscom  13143  strslfv2d  13146  basm  13165  ressval3d  13176  resseqnbasd  13177  prdsval  13377  pwsval  13395  pwsplusgval  13399  pwsmulrval  13400  imasaddvallemg  13419  xpsval  13456  plusffvalg  13466  mgm1  13474  grpidvalg  13477  sgrp1  13515  prdsidlem  13551  mnd1  13559  mnd1id  13560  subsubm  13587  grppropstrg  13623  grpinvfvalg  13646  grpsubfvalg  13649  grp1  13710  prdsinvlem  13712  pwsinvg  13716  mulgfvalg  13729  mulgnn0gsum  13736  mulg2  13739  subsubg  13805  releqgg  13828  eqgfval  13830  conjsubg  13885  gsumfzconstf  13950  mgpvalg  13958  mgpbasg  13961  mgpscag  13962  mgptopng  13964  mgpdsg  13965  mgpress  13966  ringidvalg  13996  ring1  14094  opprvalg  14104  opprmulfvalg  14105  opprbasg  14110  oppraddg  14111  subsubrng  14250  subsubrg  14281  rrgval  14298  scaffvalg  14342  lmodpropd  14385  lsssetm  14392  lsslss  14417  lspfval  14424  sraring  14485  lidlvalg  14507  rspvalg  14508  lidlss  14512  islidlm  14515  lidl0cl  14519  lidlacl  14520  lidlnegcl  14521  lidl0  14525  lidl1  14526  rspcl  14527  rspssid  14528  rsp0  14529  rspssp  14530  2idlval  14538  2idlvalg  14539  crngridl  14566  rspsn  14570  zrhval  14653  zrhvalg  14654  zlmval  14663  zlmbasg  14665  zlmplusgg  14666  zlmmulrg  14667  znval  14672  znzrh2  14682  znf1o  14687  psrval  14702  mplvalcoe  14731  mpl0fi  14743  mplnegfi  14746  tgidm  14825  tgrest  14920  ssidcn  14961  txcnmpt  15024  txcn  15026  blres  15185  mopnval  15193  remetdval  15298  expcn  15320  divccncfap  15341  cncfmet  15343  cncfcncntop  15344  hovergt0  15401  cnplimcim  15418  cnplimclemr  15420  limccnpcntop  15426  limccnp2cntop  15428  dvexp  15462  dvmptid  15467  dvmptfsum  15476  elply2  15486  elplyd  15492  plyaddlem1  15498  plymullem1  15499  plycjlemc  15511  sin0pilem1  15532  pilem3  15534  ef2kpi  15557  sin2pim  15564  cos2pim  15565  sinmpi  15566  cosmpi  15567  sinppi  15568  cosppi  15569  sinhalfpip  15571  sinhalfpim  15572  coshalfpip  15573  coshalfpim  15574  tangtx  15589  1cxp  15651  ecxp  15652  rplogb1  15699  rpelogb  15700  binom4  15730  0sgm  15736  fsumdvdsmul  15742  1sgmprm  15745  1sgm2ppw  15746  lgslem1  15756  gausslemma2dlem4  15820  lgseisenlem1  15826  lgseisenlem2  15827  lgseisenlem3  15828  lgseisenlem4  15829  lgseisen  15830  lgsquadlem1  15833  lgsquadlem2  15834  lgsquadlem3  15835  lgsquad2lem1  15837  m1lgs  15841  2lgslem3a  15849  2lgslem3b  15850  2lgslem3c  15851  2lgslem3d  15852  2sqlem8  15879  opvtxov  15901  opiedgov  15904  structiedg0val  15918  edgov  15941  edg0iedg0g  15944  upgredg  16022  usgrf1oedg  16083  ushgredgedg  16104  ushgredgedgloop  16106  griedg0ssusgr  16129  subgrprop3  16140  0uhgrsubgr  16143  vtxdgfval  16166  vtxdfifiun  16175  vtxdumgrfival  16176  vtxd0nedgbfi  16177  1hevtxdg1en  16186  upgriswlkdc  16238  wlkres  16257  trlreslem  16267  clwwlkn2  16299  eupthvdres  16353  eupth2lem3fi  16354  ex-ceil  16377  depindlem1  16384  qdencn  16690  cvgcmp2nlemabs  16695  trilpolemlt1  16704  nconstwlpolem0  16727  gfsump1  16746  gfsumcl  16747