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

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used 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  3773  rabsnif  3778  prprc2  3822  difprsn2  3855  opprc  3925  intsng  4004  riinm  4085  iinxsng  4086  iunxprg  4093  rintm  4105  sucprc  4559  unisucg  4561  xpriindim  4920  relop  4932  dmxpm  5004  riinint  5045  resabs1  5094  resabs2  5096  resima2  5099  xpssres  5100  resopab2  5113  mptimass  5142  imasng  5155  ndmima  5167  xpdisj1  5215  xpdisj2  5216  djudisj  5218  resdisj  5219  rnxpm  5220  xpima1  5237  xpima2m  5238  dmsnsnsng  5268  rnsnopg  5269  rnpropg  5270  mptiniseg  5285  dfco2a  5291  relcoi1  5322  unixpm  5326  iotaval  5352  funtp  5437  fnun  5492  fnresdisj  5496  fnima  5505  fnimaeq0  5508  fresaunres2disj  5573  fcoi1  5575  f1orescnv  5658  foun  5661  resdif  5664  tz6.12-2  5689  fveu  5690  tz6.12-1  5725  fvun2  5773  fvopab3ig  5782  f1oresrab  5876  dfmptg  5891  funopsn  5894  ressnop0  5899  fvunsng  5912  fnsnsplitss  5917  fsnunfv  5919  fvpr1  5922  fvpr2  5923  fvpr1g  5924  fvpr2g  5925  fvtp1g  5926  fvtp2g  5927  fvtp3g  5928  fvtp2  5930  fvtp3  5931  f1oiso2  6036  riotaund  6078  ovprc  6124  resoprab2  6188  fnoprabg  6192  ovidig  6209  ovigg  6212  fvmpopr2d  6228  ov6g  6230  ovconst2  6244  offval2  6322  ot1stg  6390  ot2ndg  6391  ot3rdgg  6392  opabn1stprc  6433  fmpoco  6456  algrflemg  6470  suppsnopdc  6494  tpostpos2  6540  rdgisuc1  6659  frec0g  6672  frecsuclem  6681  frecrdg  6683  oasuc  6741  oa1suc  6744  omsuc  6749  nnm1  6802  nnm2  6803  dfec2  6814  errn  6833  ixpsnval  6987  ixpintm  7011  mapen  7150  xpmapenlem  7153  phplem2  7158  undifdc  7235  prfidceq  7239  fisseneq  7246  ssfirab  7248  eqinfti  7366  infvalti  7368  infsnti  7376  casef  7434  caseinl  7437  caseinr  7438  djudom  7439  ctssdccl  7457  nninfwlpoimlemginf  7522  exmidfodomrlemim  7559  1qec  7761  mulidnq  7762  addpinq1  7837  suplocexprlem2b  8087  suplocexprlemlub  8097  0idsr  8140  1idsr  8141  caucvgsrlemoffres  8173  caucvgsr  8175  mulresr  8211  pitonnlem2  8220  ax1rid  8250  axcnre  8254  negid  8580  subneg  8582  negneg  8583  dfinfre  9294  2times  9441  infrenegsupex  10010  rexneg  10249  xaddpnf2  10266  xaddmnf1  10267  xaddmnf2  10268  fseq1p1m1  10518  fzosplitprm1  10670  infssfzcldc  10686  infssfzledc  10687  intfracq  10778  frec2uz0d  10857  frec2uzrdg  10867  frecuzrdg0  10871  frecuzrdgg  10874  frecuzrdg0t  10880  seq3val  10918  seqvalcd  10919  iseqf1olemjpcl  10966  iseqf1olemqpcl  10967  iseqf1olemfvp  10968  seq3f1olemqsum  10971  seqf1oglem2  10978  sqval  11055  iexpcyc  11102  binom3  11115  faclbnd  11201  faclbnd2  11202  bcn1  11218  hashinfom  11239  hashennn  11241  hashxp  11289  hashfibclem  11304  hashfibc  11305  hashf1lem1  11307  hashf1lem2  11308  hashtpgim  11319  hashtpglem  11320  hashtpg  11321  csbwrdg  11356  ccatlid  11396  s1val  11407  swrd00g  11443  pfxclz  11473  pfxccatpfx2  11531  cats1fvn  11558  cats1fvd  11560  cats1lend  11561  shftlem  11603  shftuz  11604  shftidt  11620  reim0  11648  remullem  11658  resqrexlemf1  11796  resqrexlemcalc3  11804  absexpzap  11869  absimle  11873  amgm2  11907  minmax  12020  mingeb  12033  2zinfmin  12034  xrmaxiflemval  12041  xrmaxadd  12052  infxrnegsupex  12054  xrminmax  12056  summodc  12175  fsum3  12179  sumsnf  12201  sumsns  12207  isumclim3  12215  isumge0  12222  fsump1i  12225  fsum2dlemstep  12226  fisumcom2  12230  fsumshftm  12237  fsumconst  12246  fsumiun  12269  hashrabrex  12273  hashuni  12274  binom11  12278  isumsplit  12283  geo2sum  12306  mertensabs  12329  prodmodc  12370  fprodseq  12375  prodsnf  12384  prodsns  12395  fprodconst  12412  fprod2dlemstep  12414  fprodcom2fi  12418  efgt1p2  12487  efgt1p  12488  resinval  12507  recosval  12508  cosadd  12529  ef01bndlem  12548  eirraplem  12569  bits0  12740  nninfctlemfo  12842  ialgr0  12847  algrp1  12849  eucalg  12862  phiprmpw  13029  phiprm  13030  prmdiv  13042  pythagtriplem12  13083  pythagtriplem14  13085  pythagtriplem16  13087  pceu  13103  pcfac  13158  prmpwdvds  13163  4sqlem5  13190  mul4sqlem  13201  ballotfilem4  13299  ballotfilem1c  13309  ballotfilemgun  13326  ennnfonelem0  13354  ennnfonelemfun  13366  ennnfonelemf1  13367  ennnfonelemrn  13368  ctinfomlemom  13376  nninfdclemp1  13399  ndxid  13434  setsfun0  13446  setsresg  13448  setscom  13450  strslfv2d  13453  basm  13472  ressval3d  13485  resseqnbasd  13486  imasaddvallemg  13695  plusffvalg  13741  mgm1  13749  grpidvalg  13752  sgrp1  13785  mnd1  13821  mnd1id  13822  subsubm  13849  grppropstrg  13883  grpinvfvalg  13906  grpsubfvalg  13909  grp1  13970  mulgfvalg  13983  mulgnn0gzsum  13990  mulg2  13993  subsubg  14059  releqgg  14082  eqgfval  14084  conjsubg  14139  cntzfval  14152  gzsumconstf  14234  gsump1  14247  gsumclfi  14249  gsummptfidmadd  14251  gsummptfidmsplit  14254  gsummptfidmsplitres  14255  gsumsnfdcmn  14257  gsumresfi  14263  gsumconstcmn  14266  gsum2d2fi  14274  prdsval  14280  prdsidlem  14300  prdsinvlem  14303  xpsval  14308  pwsval  14311  pwsplusgval  14315  pwsmulrval  14316  pwsinvg  14322  mgpvalg  14327  mgpbasg  14331  mgpscag  14333  mgptopng  14335  mgpdsg  14336  mgpress  14337  ringidvalg  14371  ring1  14471  opprvalg  14483  opprmulfvalg  14484  opprbasg  14489  oppraddg  14490  subsubrng  14631  subsubrg  14662  rrgval  14679  scaffvalg  14752  lmodpropd  14795  lsssetm  14802  lsslss  14827  lspfval  14834  sraring  14895  lidlvalg  14917  rspvalg  14918  lidlss  14922  islidlm  14925  lidl0cl  14929  lidlacl  14930  lidlnegcl  14931  lidl0  14935  lidl1  14936  rspcl  14937  rspssid  14938  rsp0  14939  rspssp  14940  2idlval  14948  2idlvalg  14949  crngridl  14976  rspsn  14980  zrhval  15061  zrhvalg  15062  zlmval  15071  zlmbasg  15073  zlmplusgg  15074  zlmmulrg  15075  znval  15080  znzrh2  15090  znf1o  15095  assapropd  15123  aspval  15124  psrval  15159  psrass1filem  15177  mplvalcoe  15206  mpl0fi  15218  mplnegfi  15221  tgidm  15300  tgrest  15395  ssidcn  15436  txcnmpt  15499  txcn  15501  blres  15660  mopnval  15668  remetdval  15773  expcn  15795  divccncfap  15816  cncfmet  15818  cncfcncntop  15819  hovergt0  15876  cnplimcim  15893  cnplimclemr  15895  limccnpcntop  15901  limccnp2cntop  15903  dvexp  15937  dvmptid  15942  dvmptfsum  15951  elply2  15961  elplyd  15967  plyaddlem1  15973  plymullem1  15974  plycjlemc  15986  sin0pilem1  16008  pilem3  16010  ef2kpi  16033  sin2pim  16040  cos2pim  16041  sinmpi  16042  cosmpi  16043  sinppi  16044  cosppi  16045  sinhalfpip  16047  sinhalfpim  16048  coshalfpip  16049  coshalfpim  16050  tangtx  16065  1cxp  16133  ecxp  16134  rplogb1  16184  rpelogb  16185  zprmlogbaplem2  16216  binom4  16219  log2tlbndlog2  16220  birthdaylem2  16226  birthdaylem3  16227  0sgm  16254  fsumdvdsmul  16285  1sgmprm  16288  1sgm2ppw  16289  ppiqub  16293  chtqub  16296  bposlem9  16319  lgslem1  16324  gausslemma2dlem4  16388  lgseisenlem1  16394  lgseisenlem2  16395  lgseisenlem3  16396  lgseisenlem4  16397  lgseisen  16398  lgsquadlem1  16401  lgsquadlem2  16402  lgsquadlem3  16403  lgsquad2lem1  16405  m1lgs  16409  2lgslem3a  16417  2lgslem3b  16418  2lgslem3c  16419  2lgslem3d  16420  2sqlem8  16447  opvtxov  16469  opiedgov  16472  structiedg0val  16486  edgov  16509  edg0iedg0g  16512  upgredg  16590  usgrf1oedg  16651  ushgredgedg  16672  ushgredgedgloop  16674  griedg0ssusgr  16697  subgrprop3  16708  0uhgrsubgr  16711  vtxdgfval  16734  vtxdfifiun  16743  vtxdumgrfival  16744  vtxd0nedgbfi  16745  1hevtxdg1en  16754  upgriswlkdc  16806  wlkres  16825  trlreslem  16835  clwwlkn2  16867  eupthvdres  16921  eupth2lem3fi  16922  ex-ceil  16945  depindlem1  16952  idjudju  17252  qdencn  17278  cvgcmp2nlemabs  17287  trilpolemlt1  17297  nconstwlpolem0  17320