Theorem eqtrid 2251

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

Syntax hints:   → wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  eqtr2id  2252  eqtr3id  2253  3eqtr3a  2263  3eqtr4g  2264  csbtt  3109  csbvarg  3125  csbie2g  3148  rabbi2dva  3385  csbprc  3510  disjssun  3528  disjpr2  3702  prprc2  3747  difprsn2  3779  opprc  3846  intsng  3925  riinm  4006  iinxsng  4007  iunxprg  4014  rintm  4026  sucprc  4467  unisucg  4469  xpriindim  4824  relop  4836  dmxpm  4907  riinint  4948  resabs1  4997  resabs2  4999  resima2  5002  xpssres  5003  resopab2  5015  mptimass  5044  imasng  5056  ndmima  5068  xpdisj1  5116  xpdisj2  5117  djudisj  5119  resdisj  5120  rnxpm  5121  xpima1  5138  xpima2m  5139  dmsnsnsng  5169  rnsnopg  5170  rnpropg  5171  mptiniseg  5186  dfco2a  5192  relcoi1  5223  unixpm  5227  iotaval  5252  funtp  5336  fnun  5391  fnresdisj  5395  fnima  5404  fnimaeq0  5407  fcoi1  5468  f1orescnv  5550  foun  5553  resdif  5556  tz6.12-2  5580  fveu  5581  tz6.12-1  5616  fvun2  5659  fvopab3ig  5666  f1oresrab  5758  dfmptg  5772  funopsn  5775  ressnop0  5778  fvunsng  5791  fnsnsplitss  5796  fsnunfv  5798  fvpr1  5801  fvpr2  5802  fvpr1g  5803  fvpr2g  5804  fvtp1g  5805  fvtp2g  5806  fvtp3g  5807  fvtp2  5809  fvtp3  5810  f1oiso2  5909  riotaund  5947  ovprc  5993  resoprab2  6055  fnoprabg  6059  ovidig  6076  ovigg  6079  fvmpopr2d  6095  ov6g  6097  ovconst2  6111  offval2  6187  ot1stg  6251  ot2ndg  6252  ot3rdgg  6253  fmpoco  6315  algrflemg  6329  tpostpos2  6364  rdgisuc1  6483  frec0g  6496  frecsuclem  6505  frecrdg  6507  oasuc  6563  oa1suc  6566  omsuc  6571  nnm1  6624  nnm2  6625  dfec2  6636  errn  6655  ixpsnval  6801  ixpintm  6825  mapen  6958  xpmapenlem  6961  phplem2  6965  undifdc  7036  prfidceq  7040  fisseneq  7046  ssfirab  7048  eqinfti  7137  infvalti  7139  infsnti  7147  casef  7205  caseinl  7208  caseinr  7209  djudom  7210  ctssdccl  7228  nninfwlpoimlemginf  7293  exmidfodomrlemim  7325  1qec  7521  mulidnq  7522  addpinq1  7597  suplocexprlem2b  7847  suplocexprlemlub  7857  0idsr  7900  1idsr  7901  caucvgsrlemoffres  7933  caucvgsr  7935  mulresr  7971  pitonnlem2  7980  ax1rid  8010  axcnre  8014  negid  8339  subneg  8341  negneg  8342  dfinfre  9049  2times  9184  infrenegsupex  9735  rexneg  9972  xaddpnf2  9989  xaddmnf1  9990  xaddmnf2  9991  fseq1p1m1  10236  fzosplitprm1  10385  intfracq  10487  frec2uz0d  10566  frec2uzrdg  10576  frecuzrdg0  10580  frecuzrdgg  10583  frecuzrdg0t  10589  seq3val  10627  seqvalcd  10628  iseqf1olemjpcl  10675  iseqf1olemqpcl  10676  iseqf1olemfvp  10677  seq3f1olemqsum  10680  seqf1oglem2  10687  sqval  10764  iexpcyc  10811  binom3  10824  faclbnd  10908  faclbnd2  10909  bcn1  10925  hashinfom  10945  hashennn  10947  hashxp  10993  csbwrdg  11045  ccatlid  11085  s1val  11094  swrd00g  11125  pfxclz  11155  shftlem  11202  shftuz  11203  shftidt  11219  reim0  11247  remullem  11257  resqrexlemf1  11394  resqrexlemcalc3  11402  absexpzap  11466  absimle  11470  amgm2  11504  minmax  11616  mingeb  11628  2zinfmin  11629  xrmaxiflemval  11636  xrmaxadd  11647  infxrnegsupex  11649  xrminmax  11651  summodc  11769  fsum3  11773  sumsnf  11795  sumsns  11801  isumclim3  11809  isumge0  11816  fsump1i  11819  fsum2dlemstep  11820  fisumcom2  11824  fsumshftm  11831  fsumconst  11840  fsumiun  11863  hashrabrex  11867  hashuni  11868  binom11  11872  isumsplit  11877  geo2sum  11900  mertensabs  11923  prodmodc  11964  fprodseq  11969  prodsnf  11978  prodsns  11989  fprodconst  12006  fprod2dlemstep  12008  fprodcom2fi  12012  efgt1p2  12081  efgt1p  12082  resinval  12101  recosval  12102  cosadd  12123  ef01bndlem  12142  eirraplem  12163  bits0  12334  nninfctlemfo  12436  ialgr0  12441  algrp1  12443  eucalg  12456  phiprmpw  12619  phiprm  12620  prmdiv  12632  pythagtriplem12  12673  pythagtriplem14  12675  pythagtriplem16  12677  pceu  12693  pcfac  12748  prmpwdvds  12753  4sqlem5  12780  mul4sqlem  12791  ennnfonelem0  12851  ennnfonelemfun  12863  ennnfonelemf1  12864  ennnfonelemrn  12865  ctinfomlemom  12873  nninfdclemp1  12896  ndxid  12931  setsfun0  12943  setsresg  12945  setscom  12947  strslfv2d  12950  basm  12968  ressval3d  12979  resseqnbasd  12980  prdsval  13180  pwsval  13198  pwsplusgval  13202  pwsmulrval  13203  imasaddvallemg  13222  xpsval  13259  plusffvalg  13269  mgm1  13277  grpidvalg  13280  sgrp1  13318  prdsidlem  13354  mnd1  13362  mnd1id  13363  subsubm  13390  grppropstrg  13426  grpinvfvalg  13449  grpsubfvalg  13452  grp1  13513  prdsinvlem  13515  pwsinvg  13519  mulgfvalg  13532  mulgnn0gsum  13539  mulg2  13542  subsubg  13608  releqgg  13631  eqgfval  13633  conjsubg  13688  gsumfzconstf  13753  mgpvalg  13760  mgpbasg  13763  mgpscag  13764  mgptopng  13766  mgpdsg  13767  mgpress  13768  ringidvalg  13798  ring1  13896  opprvalg  13906  opprmulfvalg  13907  opprbasg  13912  oppraddg  13913  subsubrng  14051  subsubrg  14082  rrgval  14099  scaffvalg  14143  lmodpropd  14186  lsssetm  14193  lsslss  14218  lspfval  14225  sraring  14286  lidlvalg  14308  rspvalg  14309  lidlss  14313  islidlm  14316  lidl0cl  14320  lidlacl  14321  lidlnegcl  14322  lidl0  14326  lidl1  14327  rspcl  14328  rspssid  14329  rsp0  14330  rspssp  14331  2idlval  14339  2idlvalg  14340  crngridl  14367  rspsn  14371  zrhval  14454  zrhvalg  14455  zlmval  14464  zlmbasg  14466  zlmplusgg  14467  zlmmulrg  14468  znval  14473  znzrh2  14483  znf1o  14488  psrval  14503  mplvalcoe  14527  mpl0fi  14539  mplnegfi  14542  tgidm  14621  tgrest  14716  ssidcn  14757  txcnmpt  14820  txcn  14822  blres  14981  mopnval  14989  remetdval  15094  expcn  15116  divccncfap  15137  cncfmet  15139  cncfcncntop  15140  hovergt0  15197  cnplimcim  15214  cnplimclemr  15216  limccnpcntop  15222  limccnp2cntop  15224  dvexp  15258  dvmptid  15263  dvmptfsum  15272  elply2  15282  elplyd  15288  plyaddlem1  15294  plymullem1  15295  plycjlemc  15307  sin0pilem1  15328  pilem3  15330  ef2kpi  15353  sin2pim  15360  cos2pim  15361  sinmpi  15362  cosmpi  15363  sinppi  15364  cosppi  15365  sinhalfpip  15367  sinhalfpim  15368  coshalfpip  15369  coshalfpim  15370  tangtx  15385  1cxp  15447  ecxp  15448  rplogb1  15495  rpelogb  15496  binom4  15526  0sgm  15532  fsumdvdsmul  15538  1sgmprm  15541  1sgm2ppw  15542  lgslem1  15552  gausslemma2dlem4  15616  lgseisenlem1  15622  lgseisenlem2  15623  lgseisenlem3  15624  lgseisenlem4  15625  lgseisen  15626  lgsquadlem1  15629  lgsquadlem2  15630  lgsquadlem3  15631  lgsquad2lem1  15633  m1lgs  15637  2lgslem3a  15645  2lgslem3b  15646  2lgslem3c  15647  2lgslem3d  15648  2sqlem8  15675  opvtxov  15697  opiedgov  15700  structiedg0val  15714  edgov  15734  edg0iedg0g  15737  ex-ceil  15801  qdencn  16107  cvgcmp2nlemabs  16112  trilpolemlt1  16121  nconstwlpolem0  16143