Theorem eqtrid 2279

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

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  eqtr2id  2280  eqtr3id  2281  3eqtr3a  2291  3eqtr4g  2292  eqab  2369  csbtt  3152  csbvarg  3168  csbie2g  3191  rabbi2dva  3431  csbprc  3556  disjssun  3574  disjpr2  3755  rabsnif  3760  prprc2  3803  difprsn2  3836  opprc  3906  intsng  3985  riinm  4066  iinxsng  4067  iunxprg  4074  rintm  4086  sucprc  4535  unisucg  4537  xpriindim  4895  relop  4907  dmxpm  4979  riinint  5020  resabs1  5069  resabs2  5071  resima2  5074  xpssres  5075  resopab2  5087  mptimass  5116  imasng  5129  ndmima  5141  xpdisj1  5189  xpdisj2  5190  djudisj  5192  resdisj  5193  rnxpm  5194  xpima1  5211  xpima2m  5212  dmsnsnsng  5242  rnsnopg  5243  rnpropg  5244  mptiniseg  5259  dfco2a  5265  relcoi1  5296  unixpm  5300  iotaval  5326  funtp  5411  fnun  5466  fnresdisj  5470  fnima  5479  fnimaeq0  5482  fresaunres2disj  5547  fcoi1  5549  f1orescnv  5632  foun  5635  resdif  5638  tz6.12-2  5663  fveu  5664  tz6.12-1  5699  fvun2  5746  fvopab3ig  5753  f1oresrab  5844  dfmptg  5859  funopsn  5862  ressnop0  5867  fvunsng  5880  fnsnsplitss  5885  fsnunfv  5887  fvpr1  5890  fvpr2  5891  fvpr1g  5892  fvpr2g  5893  fvtp1g  5894  fvtp2g  5895  fvtp3g  5896  fvtp2  5898  fvtp3  5899  f1oiso2  6002  riotaund  6042  ovprc  6088  resoprab2  6152  fnoprabg  6156  ovidig  6173  ovigg  6176  fvmpopr2d  6192  ov6g  6194  ovconst2  6208  offval2  6284  ot1stg  6348  ot2ndg  6349  ot3rdgg  6350  opabn1stprc  6391  fmpoco  6414  algrflemg  6428  suppsnopdc  6452  tpostpos2  6498  rdgisuc1  6617  frec0g  6630  frecsuclem  6639  frecrdg  6641  oasuc  6699  oa1suc  6702  omsuc  6707  nnm1  6760  nnm2  6761  dfec2  6772  errn  6791  ixpsnval  6938  ixpintm  6962  mapen  7101  xpmapenlem  7104  phplem2  7109  undifdc  7186  prfidceq  7190  fisseneq  7197  ssfirab  7199  eqinfti  7313  infvalti  7315  infsnti  7323  casef  7381  caseinl  7384  caseinr  7385  djudom  7386  ctssdccl  7404  nninfwlpoimlemginf  7469  exmidfodomrlemim  7506  1qec  7705  mulidnq  7706  addpinq1  7781  suplocexprlem2b  8031  suplocexprlemlub  8041  0idsr  8084  1idsr  8085  caucvgsrlemoffres  8117  caucvgsr  8119  mulresr  8155  pitonnlem2  8164  ax1rid  8194  axcnre  8198  negid  8522  subneg  8524  negneg  8525  dfinfre  9232  2times  9367  infrenegsupex  9929  rexneg  10166  xaddpnf2  10183  xaddmnf1  10184  xaddmnf2  10185  fseq1p1m1  10432  fzosplitprm1  10584  intfracq  10686  frec2uz0d  10765  frec2uzrdg  10775  frecuzrdg0  10779  frecuzrdgg  10782  frecuzrdg0t  10788  seq3val  10826  seqvalcd  10827  iseqf1olemjpcl  10874  iseqf1olemqpcl  10875  iseqf1olemfvp  10876  seq3f1olemqsum  10879  seqf1oglem2  10886  sqval  10963  iexpcyc  11010  binom3  11023  faclbnd  11107  faclbnd2  11108  bcn1  11124  hashinfom  11145  hashennn  11147  hashxp  11195  hashfibclem  11210  hashfibc  11211  hashtpgim  11221  hashtpglem  11222  hashtpg  11223  csbwrdg  11258  ccatlid  11298  s1val  11309  swrd00g  11345  pfxclz  11375  pfxccatpfx2  11433  cats1fvn  11460  cats1fvd  11462  cats1lend  11463  shftlem  11505  shftuz  11506  shftidt  11522  reim0  11550  remullem  11560  resqrexlemf1  11697  resqrexlemcalc3  11705  absexpzap  11769  absimle  11773  amgm2  11807  minmax  11919  mingeb  11931  2zinfmin  11932  xrmaxiflemval  11939  xrmaxadd  11950  infxrnegsupex  11952  xrminmax  11954  summodc  12073  fsum3  12077  sumsnf  12099  sumsns  12105  isumclim3  12113  isumge0  12120  fsump1i  12123  fsum2dlemstep  12124  fisumcom2  12128  fsumshftm  12135  fsumconst  12144  fsumiun  12167  hashrabrex  12171  hashuni  12172  binom11  12176  isumsplit  12181  geo2sum  12204  mertensabs  12227  prodmodc  12268  fprodseq  12273  prodsnf  12282  prodsns  12293  fprodconst  12310  fprod2dlemstep  12312  fprodcom2fi  12316  efgt1p2  12385  efgt1p  12386  resinval  12405  recosval  12406  cosadd  12427  ef01bndlem  12446  eirraplem  12467  bits0  12638  nninfctlemfo  12740  ialgr0  12745  algrp1  12747  eucalg  12760  phiprmpw  12923  phiprm  12924  prmdiv  12936  pythagtriplem12  12977  pythagtriplem14  12979  pythagtriplem16  12981  pceu  12997  pcfac  13052  prmpwdvds  13057  4sqlem5  13084  mul4sqlem  13095  ballotfilem4  13159  ennnfonelem0  13173  ennnfonelemfun  13185  ennnfonelemf1  13186  ennnfonelemrn  13187  ctinfomlemom  13195  nninfdclemp1  13218  ndxid  13253  setsfun0  13265  setsresg  13267  setscom  13269  strslfv2d  13272  basm  13291  ressval3d  13302  resseqnbasd  13303  prdsval  13503  pwsval  13521  pwsplusgval  13525  pwsmulrval  13526  imasaddvallemg  13545  xpsval  13582  plusffvalg  13592  mgm1  13600  grpidvalg  13603  sgrp1  13641  prdsidlem  13677  mnd1  13685  mnd1id  13686  subsubm  13713  grppropstrg  13749  grpinvfvalg  13772  grpsubfvalg  13775  grp1  13836  prdsinvlem  13838  pwsinvg  13842  mulgfvalg  13855  mulgnn0gsum  13862  mulg2  13865  subsubg  13931  releqgg  13954  eqgfval  13956  conjsubg  14011  gsumfzconstf  14076  mgpvalg  14084  mgpbasg  14087  mgpscag  14088  mgptopng  14090  mgpdsg  14091  mgpress  14092  ringidvalg  14122  ring1  14220  opprvalg  14230  opprmulfvalg  14231  opprbasg  14236  oppraddg  14237  subsubrng  14376  subsubrg  14407  rrgval  14424  scaffvalg  14471  lmodpropd  14514  lsssetm  14521  lsslss  14546  lspfval  14553  sraring  14614  lidlvalg  14636  rspvalg  14637  lidlss  14641  islidlm  14644  lidl0cl  14648  lidlacl  14649  lidlnegcl  14650  lidl0  14654  lidl1  14655  rspcl  14656  rspssid  14657  rsp0  14658  rspssp  14659  2idlval  14667  2idlvalg  14668  crngridl  14695  rspsn  14699  zrhval  14782  zrhvalg  14783  zlmval  14792  zlmbasg  14794  zlmplusgg  14795  zlmmulrg  14796  znval  14801  znzrh2  14811  znf1o  14816  psrval  14831  mplvalcoe  14862  mpl0fi  14874  mplnegfi  14877  tgidm  14956  tgrest  15051  ssidcn  15092  txcnmpt  15155  txcn  15157  blres  15316  mopnval  15324  remetdval  15429  expcn  15451  divccncfap  15472  cncfmet  15474  cncfcncntop  15475  hovergt0  15532  cnplimcim  15549  cnplimclemr  15551  limccnpcntop  15557  limccnp2cntop  15559  dvexp  15593  dvmptid  15598  dvmptfsum  15607  elply2  15617  elplyd  15623  plyaddlem1  15629  plymullem1  15630  plycjlemc  15642  sin0pilem1  15663  pilem3  15665  ef2kpi  15688  sin2pim  15695  cos2pim  15696  sinmpi  15697  cosmpi  15698  sinppi  15699  cosppi  15700  sinhalfpip  15702  sinhalfpim  15703  coshalfpip  15704  coshalfpim  15705  tangtx  15720  1cxp  15782  ecxp  15783  rplogb1  15830  rpelogb  15831  binom4  15861  0sgm  15870  fsumdvdsmul  15876  1sgmprm  15879  1sgm2ppw  15880  lgslem1  15890  gausslemma2dlem4  15954  lgseisenlem1  15960  lgseisenlem2  15961  lgseisenlem3  15962  lgseisenlem4  15963  lgseisen  15964  lgsquadlem1  15967  lgsquadlem2  15968  lgsquadlem3  15969  lgsquad2lem1  15971  m1lgs  15975  2lgslem3a  15983  2lgslem3b  15984  2lgslem3c  15985  2lgslem3d  15986  2sqlem8  16013  opvtxov  16035  opiedgov  16038  structiedg0val  16052  edgov  16075  edg0iedg0g  16078  upgredg  16156  usgrf1oedg  16217  ushgredgedg  16238  ushgredgedgloop  16240  griedg0ssusgr  16263  subgrprop3  16274  0uhgrsubgr  16277  vtxdgfval  16300  vtxdfifiun  16309  vtxdumgrfival  16310  vtxd0nedgbfi  16311  1hevtxdg1en  16320  upgriswlkdc  16372  wlkres  16391  trlreslem  16401  clwwlkn2  16433  eupthvdres  16487  eupth2lem3fi  16488  ex-ceil  16511  depindlem1  16518  qdencn  16824  cvgcmp2nlemabs  16833  trilpolemlt1  16842  nconstwlpolem0  16866  gfsump1  16885  gfsumcl  16887