Theorem eqtrid 2241

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

Syntax hints:   → wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  eqtr2id  2242  eqtr3id  2243  3eqtr3a  2253  3eqtr4g  2254  csbtt  3096  csbvarg  3112  csbie2g  3135  rabbi2dva  3372  csbprc  3497  disjssun  3515  disjpr2  3687  prprc2  3732  difprsn2  3763  opprc  3830  intsng  3909  riinm  3990  iinxsng  3991  iunxprg  3998  rintm  4010  sucprc  4448  unisucg  4450  xpriindim  4805  relop  4817  dmxpm  4887  riinint  4928  resabs1  4976  resabs2  4978  resima2  4981  xpssres  4982  resopab2  4994  mptimass  5023  imasng  5035  ndmima  5047  xpdisj1  5095  xpdisj2  5096  djudisj  5098  resdisj  5099  rnxpm  5100  xpima1  5117  xpima2m  5118  dmsnsnsng  5148  rnsnopg  5149  rnpropg  5150  mptiniseg  5165  dfco2a  5171  relcoi1  5202  unixpm  5206  iotaval  5231  funtp  5312  fnun  5367  fnresdisj  5371  fnima  5379  fnimaeq0  5382  fcoi1  5441  f1orescnv  5523  foun  5526  resdif  5529  tz6.12-2  5552  fveu  5553  tz6.12-1  5588  fvun2  5631  fvopab3ig  5638  f1oresrab  5730  dfmptg  5744  ressnop0  5746  fvunsng  5759  fnsnsplitss  5764  fsnunfv  5766  fvpr1  5769  fvpr2  5770  fvpr1g  5771  fvpr2g  5772  fvtp1g  5773  fvtp2g  5774  fvtp3g  5775  fvtp2  5777  fvtp3  5778  f1oiso2  5877  riotaund  5915  ovprc  5961  resoprab2  6023  fnoprabg  6027  ovidig  6044  ovigg  6047  fvmpopr2d  6063  ov6g  6065  ovconst2  6079  offval2  6155  ot1stg  6219  ot2ndg  6220  ot3rdgg  6221  fmpoco  6283  algrflemg  6297  tpostpos2  6332  rdgisuc1  6451  frec0g  6464  frecsuclem  6473  frecrdg  6475  oasuc  6531  oa1suc  6534  omsuc  6539  nnm1  6592  nnm2  6593  dfec2  6604  errn  6623  ixpsnval  6769  ixpintm  6793  mapen  6916  xpmapenlem  6919  phplem2  6923  undifdc  6994  prfidceq  6998  fisseneq  7004  ssfirab  7006  eqinfti  7095  infvalti  7097  infsnti  7105  casef  7163  caseinl  7166  caseinr  7167  djudom  7168  ctssdccl  7186  nninfwlpoimlemginf  7251  exmidfodomrlemim  7282  1qec  7474  mulidnq  7475  addpinq1  7550  suplocexprlem2b  7800  suplocexprlemlub  7810  0idsr  7853  1idsr  7854  caucvgsrlemoffres  7886  caucvgsr  7888  mulresr  7924  pitonnlem2  7933  ax1rid  7963  axcnre  7967  negid  8292  subneg  8294  negneg  8295  dfinfre  9002  2times  9137  infrenegsupex  9687  rexneg  9924  xaddpnf2  9941  xaddmnf1  9942  xaddmnf2  9943  fseq1p1m1  10188  fzosplitprm1  10329  intfracq  10431  frec2uz0d  10510  frec2uzrdg  10520  frecuzrdg0  10524  frecuzrdgg  10527  frecuzrdg0t  10533  seq3val  10571  seqvalcd  10572  iseqf1olemjpcl  10619  iseqf1olemqpcl  10620  iseqf1olemfvp  10621  seq3f1olemqsum  10624  seqf1oglem2  10631  sqval  10708  iexpcyc  10755  binom3  10768  faclbnd  10852  faclbnd2  10853  bcn1  10869  hashinfom  10889  hashennn  10891  hashxp  10937  csbwrdg  10983  shftlem  11000  shftuz  11001  shftidt  11017  reim0  11045  remullem  11055  resqrexlemf1  11192  resqrexlemcalc3  11200  absexpzap  11264  absimle  11268  amgm2  11302  minmax  11414  mingeb  11426  2zinfmin  11427  xrmaxiflemval  11434  xrmaxadd  11445  infxrnegsupex  11447  xrminmax  11449  summodc  11567  fsum3  11571  sumsnf  11593  sumsns  11599  isumclim3  11607  isumge0  11614  fsump1i  11617  fsum2dlemstep  11618  fisumcom2  11622  fsumshftm  11629  fsumconst  11638  fsumiun  11661  hashrabrex  11665  hashuni  11666  binom11  11670  isumsplit  11675  geo2sum  11698  mertensabs  11721  prodmodc  11762  fprodseq  11767  prodsnf  11776  prodsns  11787  fprodconst  11804  fprod2dlemstep  11806  fprodcom2fi  11810  efgt1p2  11879  efgt1p  11880  resinval  11899  recosval  11900  cosadd  11921  ef01bndlem  11940  eirraplem  11961  bits0  12132  nninfctlemfo  12234  ialgr0  12239  algrp1  12241  eucalg  12254  phiprmpw  12417  phiprm  12418  prmdiv  12430  pythagtriplem12  12471  pythagtriplem14  12473  pythagtriplem16  12475  pceu  12491  pcfac  12546  prmpwdvds  12551  4sqlem5  12578  mul4sqlem  12589  ennnfonelem0  12649  ennnfonelemfun  12661  ennnfonelemf1  12662  ennnfonelemrn  12663  ctinfomlemom  12671  nninfdclemp1  12694  ndxid  12729  setsfun0  12741  setsresg  12743  setscom  12745  strslfv2d  12748  basm  12766  ressval3d  12777  resseqnbasd  12778  prdsval  12977  pwsval  12995  pwsplusgval  12999  pwsmulrval  13000  imasaddvallemg  13019  xpsval  13056  plusffvalg  13066  mgm1  13074  grpidvalg  13077  sgrp1  13115  prdsidlem  13151  mnd1  13159  mnd1id  13160  subsubm  13187  grppropstrg  13223  grpinvfvalg  13246  grpsubfvalg  13249  grp1  13310  prdsinvlem  13312  pwsinvg  13316  mulgfvalg  13329  mulgnn0gsum  13336  mulg2  13339  subsubg  13405  releqgg  13428  eqgfval  13430  conjsubg  13485  gsumfzconstf  13550  mgpvalg  13557  mgpbasg  13560  mgpscag  13561  mgptopng  13563  mgpdsg  13564  mgpress  13565  ringidvalg  13595  ring1  13693  opprvalg  13703  opprmulfvalg  13704  opprbasg  13709  oppraddg  13710  subsubrng  13848  subsubrg  13879  rrgval  13896  scaffvalg  13940  lmodpropd  13983  lsssetm  13990  lsslss  14015  lspfval  14022  sraring  14083  lidlvalg  14105  rspvalg  14106  lidlss  14110  islidlm  14113  lidl0cl  14117  lidlacl  14118  lidlnegcl  14119  lidl0  14123  lidl1  14124  rspcl  14125  rspssid  14126  rsp0  14127  rspssp  14128  2idlval  14136  2idlvalg  14137  crngridl  14164  rspsn  14168  zrhval  14251  zrhvalg  14252  zlmval  14261  zlmbasg  14263  zlmplusgg  14264  zlmmulrg  14265  znval  14270  znzrh2  14280  znf1o  14285  psrval  14300  mplvalcoe  14324  mpl0fi  14336  mplnegfi  14339  tgidm  14418  tgrest  14513  ssidcn  14554  txcnmpt  14617  txcn  14619  blres  14778  mopnval  14786  remetdval  14891  expcn  14913  divccncfap  14934  cncfmet  14936  cncfcncntop  14937  hovergt0  14994  cnplimcim  15011  cnplimclemr  15013  limccnpcntop  15019  limccnp2cntop  15021  dvexp  15055  dvmptid  15060  dvmptfsum  15069  elply2  15079  elplyd  15085  plyaddlem1  15091  plymullem1  15092  plycjlemc  15104  sin0pilem1  15125  pilem3  15127  ef2kpi  15150  sin2pim  15157  cos2pim  15158  sinmpi  15159  cosmpi  15160  sinppi  15161  cosppi  15162  sinhalfpip  15164  sinhalfpim  15165  coshalfpip  15166  coshalfpim  15167  tangtx  15182  1cxp  15244  ecxp  15245  rplogb1  15292  rpelogb  15293  binom4  15323  0sgm  15329  fsumdvdsmul  15335  1sgmprm  15338  1sgm2ppw  15339  lgslem1  15349  gausslemma2dlem4  15413  lgseisenlem1  15419  lgseisenlem2  15420  lgseisenlem3  15421  lgseisenlem4  15422  lgseisen  15423  lgsquadlem1  15426  lgsquadlem2  15427  lgsquadlem3  15428  lgsquad2lem1  15430  m1lgs  15434  2lgslem3a  15442  2lgslem3b  15443  2lgslem3c  15444  2lgslem3d  15445  2sqlem8  15472  ex-ceil  15480  qdencn  15784  cvgcmp2nlemabs  15789  trilpolemlt1  15798  nconstwlpolem0  15820