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  3775  difprsn2  3807  opprc  3877  intsng  3956  riinm  4037  iinxsng  4038  iunxprg  4045  rintm  4057  sucprc  4502  unisucg  4504  xpriindim  4859  relop  4871  dmxpm  4943  riinint  4984  resabs1  5033  resabs2  5035  resima2  5038  xpssres  5039  resopab2  5051  mptimass  5080  imasng  5092  ndmima  5104  xpdisj1  5152  xpdisj2  5153  djudisj  5155  resdisj  5156  rnxpm  5157  xpima1  5174  xpima2m  5175  dmsnsnsng  5205  rnsnopg  5206  rnpropg  5207  mptiniseg  5222  dfco2a  5228  relcoi1  5259  unixpm  5263  iotaval  5289  funtp  5373  fnun  5428  fnresdisj  5432  fnima  5441  fnimaeq0  5444  fcoi1  5505  f1orescnv  5587  foun  5590  resdif  5593  tz6.12-2  5617  fveu  5618  tz6.12-1  5653  fvun2  5700  fvopab3ig  5707  f1oresrab  5799  dfmptg  5813  funopsn  5816  ressnop0  5819  fvunsng  5832  fnsnsplitss  5837  fsnunfv  5839  fvpr1  5842  fvpr2  5843  fvpr1g  5844  fvpr2g  5845  fvtp1g  5846  fvtp2g  5847  fvtp3g  5848  fvtp2  5850  fvtp3  5851  f1oiso2  5950  riotaund  5990  ovprc  6036  resoprab2  6100  fnoprabg  6104  ovidig  6121  ovigg  6124  fvmpopr2d  6140  ov6g  6142  ovconst2  6156  offval2  6232  ot1stg  6296  ot2ndg  6297  ot3rdgg  6298  fmpoco  6360  algrflemg  6374  tpostpos2  6409  rdgisuc1  6528  frec0g  6541  frecsuclem  6550  frecrdg  6552  oasuc  6608  oa1suc  6611  omsuc  6616  nnm1  6669  nnm2  6670  dfec2  6681  errn  6700  ixpsnval  6846  ixpintm  6870  mapen  7003  xpmapenlem  7006  phplem2  7010  undifdc  7082  prfidceq  7086  fisseneq  7092  ssfirab  7094  eqinfti  7183  infvalti  7185  infsnti  7193  casef  7251  caseinl  7254  caseinr  7255  djudom  7256  ctssdccl  7274  nninfwlpoimlemginf  7339  exmidfodomrlemim  7375  1qec  7571  mulidnq  7572  addpinq1  7647  suplocexprlem2b  7897  suplocexprlemlub  7907  0idsr  7950  1idsr  7951  caucvgsrlemoffres  7983  caucvgsr  7985  mulresr  8021  pitonnlem2  8030  ax1rid  8060  axcnre  8064  negid  8389  subneg  8391  negneg  8392  dfinfre  9099  2times  9234  infrenegsupex  9785  rexneg  10022  xaddpnf2  10039  xaddmnf1  10040  xaddmnf2  10041  fseq1p1m1  10286  fzosplitprm1  10435  intfracq  10537  frec2uz0d  10616  frec2uzrdg  10626  frecuzrdg0  10630  frecuzrdgg  10633  frecuzrdg0t  10639  seq3val  10677  seqvalcd  10678  iseqf1olemjpcl  10725  iseqf1olemqpcl  10726  iseqf1olemfvp  10727  seq3f1olemqsum  10730  seqf1oglem2  10737  sqval  10814  iexpcyc  10861  binom3  10874  faclbnd  10958  faclbnd2  10959  bcn1  10975  hashinfom  10995  hashennn  10997  hashxp  11043  csbwrdg  11096  ccatlid  11136  s1val  11145  swrd00g  11176  pfxclz  11206  pfxccatpfx2  11264  cats1fvn  11291  cats1fvd  11293  cats1lend  11294  shftlem  11322  shftuz  11323  shftidt  11339  reim0  11367  remullem  11377  resqrexlemf1  11514  resqrexlemcalc3  11522  absexpzap  11586  absimle  11590  amgm2  11624  minmax  11736  mingeb  11748  2zinfmin  11749  xrmaxiflemval  11756  xrmaxadd  11767  infxrnegsupex  11769  xrminmax  11771  summodc  11889  fsum3  11893  sumsnf  11915  sumsns  11921  isumclim3  11929  isumge0  11936  fsump1i  11939  fsum2dlemstep  11940  fisumcom2  11944  fsumshftm  11951  fsumconst  11960  fsumiun  11983  hashrabrex  11987  hashuni  11988  binom11  11992  isumsplit  11997  geo2sum  12020  mertensabs  12043  prodmodc  12084  fprodseq  12089  prodsnf  12098  prodsns  12109  fprodconst  12126  fprod2dlemstep  12128  fprodcom2fi  12132  efgt1p2  12201  efgt1p  12202  resinval  12221  recosval  12222  cosadd  12243  ef01bndlem  12262  eirraplem  12283  bits0  12454  nninfctlemfo  12556  ialgr0  12561  algrp1  12563  eucalg  12576  phiprmpw  12739  phiprm  12740  prmdiv  12752  pythagtriplem12  12793  pythagtriplem14  12795  pythagtriplem16  12797  pceu  12813  pcfac  12868  prmpwdvds  12873  4sqlem5  12900  mul4sqlem  12911  ennnfonelem0  12971  ennnfonelemfun  12983  ennnfonelemf1  12984  ennnfonelemrn  12985  ctinfomlemom  12993  nninfdclemp1  13016  ndxid  13051  setsfun0  13063  setsresg  13065  setscom  13067  strslfv2d  13070  basm  13089  ressval3d  13100  resseqnbasd  13101  prdsval  13301  pwsval  13319  pwsplusgval  13323  pwsmulrval  13324  imasaddvallemg  13343  xpsval  13380  plusffvalg  13390  mgm1  13398  grpidvalg  13401  sgrp1  13439  prdsidlem  13475  mnd1  13483  mnd1id  13484  subsubm  13511  grppropstrg  13547  grpinvfvalg  13570  grpsubfvalg  13573  grp1  13634  prdsinvlem  13636  pwsinvg  13640  mulgfvalg  13653  mulgnn0gsum  13660  mulg2  13663  subsubg  13729  releqgg  13752  eqgfval  13754  conjsubg  13809  gsumfzconstf  13874  mgpvalg  13881  mgpbasg  13884  mgpscag  13885  mgptopng  13887  mgpdsg  13888  mgpress  13889  ringidvalg  13919  ring1  14017  opprvalg  14027  opprmulfvalg  14028  opprbasg  14033  oppraddg  14034  subsubrng  14172  subsubrg  14203  rrgval  14220  scaffvalg  14264  lmodpropd  14307  lsssetm  14314  lsslss  14339  lspfval  14346  sraring  14407  lidlvalg  14429  rspvalg  14430  lidlss  14434  islidlm  14437  lidl0cl  14441  lidlacl  14442  lidlnegcl  14443  lidl0  14447  lidl1  14448  rspcl  14449  rspssid  14450  rsp0  14451  rspssp  14452  2idlval  14460  2idlvalg  14461  crngridl  14488  rspsn  14492  zrhval  14575  zrhvalg  14576  zlmval  14585  zlmbasg  14587  zlmplusgg  14588  zlmmulrg  14589  znval  14594  znzrh2  14604  znf1o  14609  psrval  14624  mplvalcoe  14648  mpl0fi  14660  mplnegfi  14663  tgidm  14742  tgrest  14837  ssidcn  14878  txcnmpt  14941  txcn  14943  blres  15102  mopnval  15110  remetdval  15215  expcn  15237  divccncfap  15258  cncfmet  15260  cncfcncntop  15261  hovergt0  15318  cnplimcim  15335  cnplimclemr  15337  limccnpcntop  15343  limccnp2cntop  15345  dvexp  15379  dvmptid  15384  dvmptfsum  15393  elply2  15403  elplyd  15409  plyaddlem1  15415  plymullem1  15416  plycjlemc  15428  sin0pilem1  15449  pilem3  15451  ef2kpi  15474  sin2pim  15481  cos2pim  15482  sinmpi  15483  cosmpi  15484  sinppi  15485  cosppi  15486  sinhalfpip  15488  sinhalfpim  15489  coshalfpip  15490  coshalfpim  15491  tangtx  15506  1cxp  15568  ecxp  15569  rplogb1  15616  rpelogb  15617  binom4  15647  0sgm  15653  fsumdvdsmul  15659  1sgmprm  15662  1sgm2ppw  15663  lgslem1  15673  gausslemma2dlem4  15737  lgseisenlem1  15743  lgseisenlem2  15744  lgseisenlem3  15745  lgseisenlem4  15746  lgseisen  15747  lgsquadlem1  15750  lgsquadlem2  15751  lgsquadlem3  15752  lgsquad2lem1  15754  m1lgs  15758  2lgslem3a  15766  2lgslem3b  15767  2lgslem3c  15768  2lgslem3d  15769  2sqlem8  15796  opvtxov  15818  opiedgov  15821  structiedg0val  15835  edgov  15857  edg0iedg0g  15860  upgredg  15936  usgrf1oedg  15997  ushgredgedg  16018  ushgredgedgloop  16020  ex-ceil  16048  qdencn  16354  cvgcmp2nlemabs  16359  trilpolemlt1  16368  nconstwlpolem0  16390