Theorem eqtrid 2274

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  eqtr2id  2275  eqtr3id  2276  3eqtr3a  2286  3eqtr4g  2287  csbtt  3136  csbvarg  3152  csbie2g  3175  rabbi2dva  3412  csbprc  3537  disjssun  3555  disjpr2  3730  prprc2  3776  difprsn2  3808  opprc  3878  intsng  3957  riinm  4038  iinxsng  4039  iunxprg  4046  rintm  4058  sucprc  4503  unisucg  4505  xpriindim  4860  relop  4872  dmxpm  4944  riinint  4985  resabs1  5034  resabs2  5036  resima2  5039  xpssres  5040  resopab2  5052  mptimass  5081  imasng  5093  ndmima  5105  xpdisj1  5153  xpdisj2  5154  djudisj  5156  resdisj  5157  rnxpm  5158  xpima1  5175  xpima2m  5176  dmsnsnsng  5206  rnsnopg  5207  rnpropg  5208  mptiniseg  5223  dfco2a  5229  relcoi1  5260  unixpm  5264  iotaval  5290  funtp  5374  fnun  5429  fnresdisj  5433  fnima  5442  fnimaeq0  5445  fcoi1  5508  f1orescnv  5590  foun  5593  resdif  5596  tz6.12-2  5620  fveu  5621  tz6.12-1  5656  fvun2  5703  fvopab3ig  5710  f1oresrab  5802  dfmptg  5816  funopsn  5819  ressnop0  5824  fvunsng  5837  fnsnsplitss  5842  fsnunfv  5844  fvpr1  5847  fvpr2  5848  fvpr1g  5849  fvpr2g  5850  fvtp1g  5851  fvtp2g  5852  fvtp3g  5853  fvtp2  5855  fvtp3  5856  f1oiso2  5957  riotaund  5997  ovprc  6043  resoprab2  6107  fnoprabg  6111  ovidig  6128  ovigg  6131  fvmpopr2d  6147  ov6g  6149  ovconst2  6163  offval2  6240  ot1stg  6304  ot2ndg  6305  ot3rdgg  6306  fmpoco  6368  algrflemg  6382  tpostpos2  6417  rdgisuc1  6536  frec0g  6549  frecsuclem  6558  frecrdg  6560  oasuc  6618  oa1suc  6621  omsuc  6626  nnm1  6679  nnm2  6680  dfec2  6691  errn  6710  ixpsnval  6856  ixpintm  6880  mapen  7015  xpmapenlem  7018  phplem2  7022  undifdc  7097  prfidceq  7101  fisseneq  7107  ssfirab  7109  eqinfti  7198  infvalti  7200  infsnti  7208  casef  7266  caseinl  7269  caseinr  7270  djudom  7271  ctssdccl  7289  nninfwlpoimlemginf  7354  exmidfodomrlemim  7390  1qec  7586  mulidnq  7587  addpinq1  7662  suplocexprlem2b  7912  suplocexprlemlub  7922  0idsr  7965  1idsr  7966  caucvgsrlemoffres  7998  caucvgsr  8000  mulresr  8036  pitonnlem2  8045  ax1rid  8075  axcnre  8079  negid  8404  subneg  8406  negneg  8407  dfinfre  9114  2times  9249  infrenegsupex  9801  rexneg  10038  xaddpnf2  10055  xaddmnf1  10056  xaddmnf2  10057  fseq1p1m1  10302  fzosplitprm1  10452  intfracq  10554  frec2uz0d  10633  frec2uzrdg  10643  frecuzrdg0  10647  frecuzrdgg  10650  frecuzrdg0t  10656  seq3val  10694  seqvalcd  10695  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  iseqf1olemfvp  10744  seq3f1olemqsum  10747  seqf1oglem2  10754  sqval  10831  iexpcyc  10878  binom3  10891  faclbnd  10975  faclbnd2  10976  bcn1  10992  hashinfom  11012  hashennn  11014  hashxp  11061  csbwrdg  11114  ccatlid  11154  s1val  11165  swrd00g  11196  pfxclz  11226  pfxccatpfx2  11284  cats1fvn  11311  cats1fvd  11313  cats1lend  11314  shftlem  11342  shftuz  11343  shftidt  11359  reim0  11387  remullem  11397  resqrexlemf1  11534  resqrexlemcalc3  11542  absexpzap  11606  absimle  11610  amgm2  11644  minmax  11756  mingeb  11768  2zinfmin  11769  xrmaxiflemval  11776  xrmaxadd  11787  infxrnegsupex  11789  xrminmax  11791  summodc  11909  fsum3  11913  sumsnf  11935  sumsns  11941  isumclim3  11949  isumge0  11956  fsump1i  11959  fsum2dlemstep  11960  fisumcom2  11964  fsumshftm  11971  fsumconst  11980  fsumiun  12003  hashrabrex  12007  hashuni  12008  binom11  12012  isumsplit  12017  geo2sum  12040  mertensabs  12063  prodmodc  12104  fprodseq  12109  prodsnf  12118  prodsns  12129  fprodconst  12146  fprod2dlemstep  12148  fprodcom2fi  12152  efgt1p2  12221  efgt1p  12222  resinval  12241  recosval  12242  cosadd  12263  ef01bndlem  12282  eirraplem  12303  bits0  12474  nninfctlemfo  12576  ialgr0  12581  algrp1  12583  eucalg  12596  phiprmpw  12759  phiprm  12760  prmdiv  12772  pythagtriplem12  12813  pythagtriplem14  12815  pythagtriplem16  12817  pceu  12833  pcfac  12888  prmpwdvds  12893  4sqlem5  12920  mul4sqlem  12931  ennnfonelem0  12991  ennnfonelemfun  13003  ennnfonelemf1  13004  ennnfonelemrn  13005  ctinfomlemom  13013  nninfdclemp1  13036  ndxid  13071  setsfun0  13083  setsresg  13085  setscom  13087  strslfv2d  13090  basm  13109  ressval3d  13120  resseqnbasd  13121  prdsval  13321  pwsval  13339  pwsplusgval  13343  pwsmulrval  13344  imasaddvallemg  13363  xpsval  13400  plusffvalg  13410  mgm1  13418  grpidvalg  13421  sgrp1  13459  prdsidlem  13495  mnd1  13503  mnd1id  13504  subsubm  13531  grppropstrg  13567  grpinvfvalg  13590  grpsubfvalg  13593  grp1  13654  prdsinvlem  13656  pwsinvg  13660  mulgfvalg  13673  mulgnn0gsum  13680  mulg2  13683  subsubg  13749  releqgg  13772  eqgfval  13774  conjsubg  13829  gsumfzconstf  13894  mgpvalg  13901  mgpbasg  13904  mgpscag  13905  mgptopng  13907  mgpdsg  13908  mgpress  13909  ringidvalg  13939  ring1  14037  opprvalg  14047  opprmulfvalg  14048  opprbasg  14053  oppraddg  14054  subsubrng  14193  subsubrg  14224  rrgval  14241  scaffvalg  14285  lmodpropd  14328  lsssetm  14335  lsslss  14360  lspfval  14367  sraring  14428  lidlvalg  14450  rspvalg  14451  lidlss  14455  islidlm  14458  lidl0cl  14462  lidlacl  14463  lidlnegcl  14464  lidl0  14468  lidl1  14469  rspcl  14470  rspssid  14471  rsp0  14472  rspssp  14473  2idlval  14481  2idlvalg  14482  crngridl  14509  rspsn  14513  zrhval  14596  zrhvalg  14597  zlmval  14606  zlmbasg  14608  zlmplusgg  14609  zlmmulrg  14610  znval  14615  znzrh2  14625  znf1o  14630  psrval  14645  mplvalcoe  14669  mpl0fi  14681  mplnegfi  14684  tgidm  14763  tgrest  14858  ssidcn  14899  txcnmpt  14962  txcn  14964  blres  15123  mopnval  15131  remetdval  15236  expcn  15258  divccncfap  15279  cncfmet  15281  cncfcncntop  15282  hovergt0  15339  cnplimcim  15356  cnplimclemr  15358  limccnpcntop  15364  limccnp2cntop  15366  dvexp  15400  dvmptid  15405  dvmptfsum  15414  elply2  15424  elplyd  15430  plyaddlem1  15436  plymullem1  15437  plycjlemc  15449  sin0pilem1  15470  pilem3  15472  ef2kpi  15495  sin2pim  15502  cos2pim  15503  sinmpi  15504  cosmpi  15505  sinppi  15506  cosppi  15507  sinhalfpip  15509  sinhalfpim  15510  coshalfpip  15511  coshalfpim  15512  tangtx  15527  1cxp  15589  ecxp  15590  rplogb1  15637  rpelogb  15638  binom4  15668  0sgm  15674  fsumdvdsmul  15680  1sgmprm  15683  1sgm2ppw  15684  lgslem1  15694  gausslemma2dlem4  15758  lgseisenlem1  15764  lgseisenlem2  15765  lgseisenlem3  15766  lgseisenlem4  15767  lgseisen  15768  lgsquadlem1  15771  lgsquadlem2  15772  lgsquadlem3  15773  lgsquad2lem1  15775  m1lgs  15779  2lgslem3a  15787  2lgslem3b  15788  2lgslem3c  15789  2lgslem3d  15790  2sqlem8  15817  opvtxov  15839  opiedgov  15842  structiedg0val  15856  edgov  15878  edg0iedg0g  15881  upgredg  15957  usgrf1oedg  16018  ushgredgedg  16039  ushgredgedgloop  16041  vtxdgfval  16047  vtxdfifiun  16056  vtxdumgrfival  16057  upgriswlkdc  16101  wlkres  16118  trlreslem  16127  ex-ceil  16145  qdencn  16455  cvgcmp2nlemabs  16460  trilpolemlt1  16469  nconstwlpolem0  16491