Theorem eqtrid 2283

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

Syntax hints:   → wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced 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  3772  rabsnif  3777  prprc2  3820  difprsn2  3853  opprc  3923  intsng  4002  riinm  4083  iinxsng  4084  iunxprg  4091  rintm  4103  sucprc  4555  unisucg  4557  xpriindim  4916  relop  4928  dmxpm  5000  riinint  5041  resabs1  5090  resabs2  5092  resima2  5095  xpssres  5096  resopab2  5108  mptimass  5137  imasng  5150  ndmima  5162  xpdisj1  5210  xpdisj2  5211  djudisj  5213  resdisj  5214  rnxpm  5215  xpima1  5232  xpima2m  5233  dmsnsnsng  5263  rnsnopg  5264  rnpropg  5265  mptiniseg  5280  dfco2a  5286  relcoi1  5317  unixpm  5321  iotaval  5347  funtp  5432  fnun  5487  fnresdisj  5491  fnima  5500  fnimaeq0  5503  fresaunres2disj  5568  fcoi1  5570  f1orescnv  5653  foun  5656  resdif  5659  tz6.12-2  5684  fveu  5685  tz6.12-1  5720  fvun2  5767  fvopab3ig  5776  f1oresrab  5867  dfmptg  5882  funopsn  5885  ressnop0  5890  fvunsng  5903  fnsnsplitss  5908  fsnunfv  5910  fvpr1  5913  fvpr2  5914  fvpr1g  5915  fvpr2g  5916  fvtp1g  5917  fvtp2g  5918  fvtp3g  5919  fvtp2  5921  fvtp3  5922  f1oiso2  6027  riotaund  6069  ovprc  6115  resoprab2  6179  fnoprabg  6183  ovidig  6200  ovigg  6203  fvmpopr2d  6219  ov6g  6221  ovconst2  6235  offval2  6312  ot1stg  6380  ot2ndg  6381  ot3rdgg  6382  opabn1stprc  6423  fmpoco  6446  algrflemg  6460  suppsnopdc  6484  tpostpos2  6530  rdgisuc1  6649  frec0g  6662  frecsuclem  6671  frecrdg  6673  oasuc  6731  oa1suc  6734  omsuc  6739  nnm1  6792  nnm2  6793  dfec2  6804  errn  6823  ixpsnval  6977  ixpintm  7001  mapen  7140  xpmapenlem  7143  phplem2  7148  undifdc  7225  prfidceq  7229  fisseneq  7236  ssfirab  7238  eqinfti  7354  infvalti  7356  infsnti  7364  casef  7422  caseinl  7425  caseinr  7426  djudom  7427  ctssdccl  7445  nninfwlpoimlemginf  7510  exmidfodomrlemim  7547  1qec  7749  mulidnq  7750  addpinq1  7825  suplocexprlem2b  8075  suplocexprlemlub  8085  0idsr  8128  1idsr  8129  caucvgsrlemoffres  8161  caucvgsr  8163  mulresr  8199  pitonnlem2  8208  ax1rid  8238  axcnre  8242  negid  8567  subneg  8569  negneg  8570  dfinfre  9280  2times  9415  infrenegsupex  9977  rexneg  10215  xaddpnf2  10232  xaddmnf1  10233  xaddmnf2  10234  fseq1p1m1  10484  fzosplitprm1  10636  infssfzcldc  10652  infssfzledc  10653  intfracq  10740  frec2uz0d  10819  frec2uzrdg  10829  frecuzrdg0  10833  frecuzrdgg  10836  frecuzrdg0t  10842  seq3val  10880  seqvalcd  10881  iseqf1olemjpcl  10928  iseqf1olemqpcl  10929  iseqf1olemfvp  10930  seq3f1olemqsum  10933  seqf1oglem2  10940  sqval  11017  iexpcyc  11064  binom3  11077  faclbnd  11162  faclbnd2  11163  bcn1  11179  hashinfom  11200  hashennn  11202  hashxp  11250  hashfibclem  11265  hashfibc  11266  hashf1lem1  11268  hashf1lem2  11269  hashtpgim  11280  hashtpglem  11281  hashtpg  11282  csbwrdg  11317  ccatlid  11357  s1val  11368  swrd00g  11404  pfxclz  11434  pfxccatpfx2  11492  cats1fvn  11519  cats1fvd  11521  cats1lend  11522  shftlem  11564  shftuz  11565  shftidt  11581  reim0  11609  remullem  11619  resqrexlemf1  11757  resqrexlemcalc3  11765  absexpzap  11829  absimle  11833  amgm2  11867  minmax  11979  mingeb  11991  2zinfmin  11992  xrmaxiflemval  11999  xrmaxadd  12010  infxrnegsupex  12012  xrminmax  12014  summodc  12133  fsum3  12137  sumsnf  12159  sumsns  12165  isumclim3  12173  isumge0  12180  fsump1i  12183  fsum2dlemstep  12184  fisumcom2  12188  fsumshftm  12195  fsumconst  12204  fsumiun  12227  hashrabrex  12231  hashuni  12232  binom11  12236  isumsplit  12241  geo2sum  12264  mertensabs  12287  prodmodc  12328  fprodseq  12333  prodsnf  12342  prodsns  12353  fprodconst  12370  fprod2dlemstep  12372  fprodcom2fi  12376  efgt1p2  12445  efgt1p  12446  resinval  12465  recosval  12466  cosadd  12487  ef01bndlem  12506  eirraplem  12527  bits0  12698  nninfctlemfo  12800  ialgr0  12805  algrp1  12807  eucalg  12820  phiprmpw  12983  phiprm  12984  prmdiv  12996  pythagtriplem12  13037  pythagtriplem14  13039  pythagtriplem16  13041  pceu  13057  pcfac  13112  prmpwdvds  13117  4sqlem5  13144  mul4sqlem  13155  ballotfilem4  13224  ballotfilem1c  13234  ballotfilemgun  13251  ennnfonelem0  13279  ennnfonelemfun  13291  ennnfonelemf1  13292  ennnfonelemrn  13293  ctinfomlemom  13301  nninfdclemp1  13324  ndxid  13359  setsfun0  13371  setsresg  13373  setscom  13375  strslfv2d  13378  basm  13397  ressval3d  13409  resseqnbasd  13410  imasaddvallemg  13619  plusffvalg  13665  mgm1  13673  grpidvalg  13676  sgrp1  13709  mnd1  13745  mnd1id  13746  subsubm  13773  grppropstrg  13807  grpinvfvalg  13830  grpsubfvalg  13833  grp1  13894  mulgfvalg  13907  mulgnn0gzsum  13914  mulg2  13917  subsubg  13983  releqgg  14006  eqgfval  14008  conjsubg  14063  gzsumconstf  14127  gsump1  14140  gsumclfi  14142  gsummptfidmadd  14144  gsumconstcmn  14149  prdsval  14156  prdsidlem  14176  prdsinvlem  14179  xpsval  14184  pwsval  14187  pwsplusgval  14191  pwsmulrval  14192  pwsinvg  14198  mgpvalg  14203  mgpbasg  14207  mgpscag  14209  mgptopng  14211  mgpdsg  14212  mgpress  14213  ringidvalg  14247  ring1  14347  opprvalg  14357  opprmulfvalg  14358  opprbasg  14363  oppraddg  14364  subsubrng  14505  subsubrg  14536  rrgval  14553  scaffvalg  14626  lmodpropd  14669  lsssetm  14676  lsslss  14701  lspfval  14708  sraring  14769  lidlvalg  14791  rspvalg  14792  lidlss  14796  islidlm  14799  lidl0cl  14803  lidlacl  14804  lidlnegcl  14805  lidl0  14809  lidl1  14810  rspcl  14811  rspssid  14812  rsp0  14813  rspssp  14814  2idlval  14822  2idlvalg  14823  crngridl  14850  rspsn  14854  zrhval  14935  zrhvalg  14936  zlmval  14945  zlmbasg  14947  zlmplusgg  14948  zlmmulrg  14949  znval  14954  znzrh2  14964  znf1o  14969  assapropd  14997  aspval  14998  psrval  15033  mplvalcoe  15064  mpl0fi  15076  mplnegfi  15079  tgidm  15158  tgrest  15253  ssidcn  15294  txcnmpt  15357  txcn  15359  blres  15518  mopnval  15526  remetdval  15631  expcn  15653  divccncfap  15674  cncfmet  15676  cncfcncntop  15677  hovergt0  15734  cnplimcim  15751  cnplimclemr  15753  limccnpcntop  15759  limccnp2cntop  15761  dvexp  15795  dvmptid  15800  dvmptfsum  15809  elply2  15819  elplyd  15825  plyaddlem1  15831  plymullem1  15832  plycjlemc  15844  sin0pilem1  15865  pilem3  15867  ef2kpi  15890  sin2pim  15897  cos2pim  15898  sinmpi  15899  cosmpi  15900  sinppi  15901  cosppi  15902  sinhalfpip  15904  sinhalfpim  15905  coshalfpip  15906  coshalfpim  15907  tangtx  15922  1cxp  15985  ecxp  15986  rplogb1  16033  rpelogb  16034  binom4  16064  log2tlbndlog2  16065  birthdaylem2  16071  birthdaylem3  16072  0sgm  16082  fsumdvdsmul  16088  1sgmprm  16091  1sgm2ppw  16092  lgslem1  16102  gausslemma2dlem4  16166  lgseisenlem1  16172  lgseisenlem2  16173  lgseisenlem3  16174  lgseisenlem4  16175  lgseisen  16176  lgsquadlem1  16179  lgsquadlem2  16180  lgsquadlem3  16181  lgsquad2lem1  16183  m1lgs  16187  2lgslem3a  16195  2lgslem3b  16196  2lgslem3c  16197  2lgslem3d  16198  2sqlem8  16225  opvtxov  16247  opiedgov  16250  structiedg0val  16264  edgov  16287  edg0iedg0g  16290  upgredg  16368  usgrf1oedg  16429  ushgredgedg  16450  ushgredgedgloop  16452  griedg0ssusgr  16475  subgrprop3  16486  0uhgrsubgr  16489  vtxdgfval  16512  vtxdfifiun  16521  vtxdumgrfival  16522  vtxd0nedgbfi  16523  1hevtxdg1en  16532  upgriswlkdc  16584  wlkres  16603  trlreslem  16613  clwwlkn2  16645  eupthvdres  16699  eupth2lem3fi  16700  ex-ceil  16723  depindlem1  16730  qdencn  17046  cvgcmp2nlemabs  17055  trilpolemlt1  17064  nconstwlpolem0  17087