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  3137  csbvarg  3153  csbie2g  3176  rabbi2dva  3413  csbprc  3538  disjssun  3556  disjpr2  3731  rabsnif  3736  prprc2  3779  difprsn2  3811  opprc  3881  intsng  3960  riinm  4041  iinxsng  4042  iunxprg  4049  rintm  4061  sucprc  4507  unisucg  4509  xpriindim  4866  relop  4878  dmxpm  4950  riinint  4991  resabs1  5040  resabs2  5042  resima2  5045  xpssres  5046  resopab2  5058  mptimass  5087  imasng  5099  ndmima  5111  xpdisj1  5159  xpdisj2  5160  djudisj  5162  resdisj  5163  rnxpm  5164  xpima1  5181  xpima2m  5182  dmsnsnsng  5212  rnsnopg  5213  rnpropg  5214  mptiniseg  5229  dfco2a  5235  relcoi1  5266  unixpm  5270  iotaval  5296  funtp  5380  fnun  5435  fnresdisj  5439  fnima  5448  fnimaeq0  5451  fcoi1  5514  f1orescnv  5596  foun  5599  resdif  5602  tz6.12-2  5626  fveu  5627  tz6.12-1  5662  fvun2  5709  fvopab3ig  5716  f1oresrab  5808  dfmptg  5822  funopsn  5825  ressnop0  5830  fvunsng  5843  fnsnsplitss  5848  fsnunfv  5850  fvpr1  5853  fvpr2  5854  fvpr1g  5855  fvpr2g  5856  fvtp1g  5857  fvtp2g  5858  fvtp3g  5859  fvtp2  5861  fvtp3  5862  f1oiso2  5963  riotaund  6003  ovprc  6049  resoprab2  6113  fnoprabg  6117  ovidig  6134  ovigg  6137  fvmpopr2d  6153  ov6g  6155  ovconst2  6169  offval2  6246  ot1stg  6310  ot2ndg  6311  ot3rdgg  6312  opabn1stprc  6353  fmpoco  6376  algrflemg  6390  tpostpos2  6426  rdgisuc1  6545  frec0g  6558  frecsuclem  6567  frecrdg  6569  oasuc  6627  oa1suc  6630  omsuc  6635  nnm1  6688  nnm2  6689  dfec2  6700  errn  6719  ixpsnval  6865  ixpintm  6889  mapen  7027  xpmapenlem  7030  phplem2  7034  undifdc  7109  prfidceq  7113  fisseneq  7119  ssfirab  7121  eqinfti  7210  infvalti  7212  infsnti  7220  casef  7278  caseinl  7281  caseinr  7282  djudom  7283  ctssdccl  7301  nninfwlpoimlemginf  7366  exmidfodomrlemim  7402  1qec  7598  mulidnq  7599  addpinq1  7674  suplocexprlem2b  7924  suplocexprlemlub  7934  0idsr  7977  1idsr  7978  caucvgsrlemoffres  8010  caucvgsr  8012  mulresr  8048  pitonnlem2  8057  ax1rid  8087  axcnre  8091  negid  8416  subneg  8418  negneg  8419  dfinfre  9126  2times  9261  infrenegsupex  9818  rexneg  10055  xaddpnf2  10072  xaddmnf1  10073  xaddmnf2  10074  fseq1p1m1  10319  fzosplitprm1  10470  intfracq  10572  frec2uz0d  10651  frec2uzrdg  10661  frecuzrdg0  10665  frecuzrdgg  10668  frecuzrdg0t  10674  seq3val  10712  seqvalcd  10713  iseqf1olemjpcl  10760  iseqf1olemqpcl  10761  iseqf1olemfvp  10762  seq3f1olemqsum  10765  seqf1oglem2  10772  sqval  10849  iexpcyc  10896  binom3  10909  faclbnd  10993  faclbnd2  10994  bcn1  11010  hashinfom  11030  hashennn  11032  hashxp  11080  csbwrdg  11133  ccatlid  11173  s1val  11184  swrd00g  11220  pfxclz  11250  pfxccatpfx2  11308  cats1fvn  11335  cats1fvd  11337  cats1lend  11338  shftlem  11367  shftuz  11368  shftidt  11384  reim0  11412  remullem  11422  resqrexlemf1  11559  resqrexlemcalc3  11567  absexpzap  11631  absimle  11635  amgm2  11669  minmax  11781  mingeb  11793  2zinfmin  11794  xrmaxiflemval  11801  xrmaxadd  11812  infxrnegsupex  11814  xrminmax  11816  summodc  11934  fsum3  11938  sumsnf  11960  sumsns  11966  isumclim3  11974  isumge0  11981  fsump1i  11984  fsum2dlemstep  11985  fisumcom2  11989  fsumshftm  11996  fsumconst  12005  fsumiun  12028  hashrabrex  12032  hashuni  12033  binom11  12037  isumsplit  12042  geo2sum  12065  mertensabs  12088  prodmodc  12129  fprodseq  12134  prodsnf  12143  prodsns  12154  fprodconst  12171  fprod2dlemstep  12173  fprodcom2fi  12177  efgt1p2  12246  efgt1p  12247  resinval  12266  recosval  12267  cosadd  12288  ef01bndlem  12307  eirraplem  12328  bits0  12499  nninfctlemfo  12601  ialgr0  12606  algrp1  12608  eucalg  12621  phiprmpw  12784  phiprm  12785  prmdiv  12797  pythagtriplem12  12838  pythagtriplem14  12840  pythagtriplem16  12842  pceu  12858  pcfac  12913  prmpwdvds  12918  4sqlem5  12945  mul4sqlem  12956  ennnfonelem0  13016  ennnfonelemfun  13028  ennnfonelemf1  13029  ennnfonelemrn  13030  ctinfomlemom  13038  nninfdclemp1  13061  ndxid  13096  setsfun0  13108  setsresg  13110  setscom  13112  strslfv2d  13115  basm  13134  ressval3d  13145  resseqnbasd  13146  prdsval  13346  pwsval  13364  pwsplusgval  13368  pwsmulrval  13369  imasaddvallemg  13388  xpsval  13425  plusffvalg  13435  mgm1  13443  grpidvalg  13446  sgrp1  13484  prdsidlem  13520  mnd1  13528  mnd1id  13529  subsubm  13556  grppropstrg  13592  grpinvfvalg  13615  grpsubfvalg  13618  grp1  13679  prdsinvlem  13681  pwsinvg  13685  mulgfvalg  13698  mulgnn0gsum  13705  mulg2  13708  subsubg  13774  releqgg  13797  eqgfval  13799  conjsubg  13854  gsumfzconstf  13919  mgpvalg  13926  mgpbasg  13929  mgpscag  13930  mgptopng  13932  mgpdsg  13933  mgpress  13934  ringidvalg  13964  ring1  14062  opprvalg  14072  opprmulfvalg  14073  opprbasg  14078  oppraddg  14079  subsubrng  14218  subsubrg  14249  rrgval  14266  scaffvalg  14310  lmodpropd  14353  lsssetm  14360  lsslss  14385  lspfval  14392  sraring  14453  lidlvalg  14475  rspvalg  14476  lidlss  14480  islidlm  14483  lidl0cl  14487  lidlacl  14488  lidlnegcl  14489  lidl0  14493  lidl1  14494  rspcl  14495  rspssid  14496  rsp0  14497  rspssp  14498  2idlval  14506  2idlvalg  14507  crngridl  14534  rspsn  14538  zrhval  14621  zrhvalg  14622  zlmval  14631  zlmbasg  14633  zlmplusgg  14634  zlmmulrg  14635  znval  14640  znzrh2  14650  znf1o  14655  psrval  14670  mplvalcoe  14694  mpl0fi  14706  mplnegfi  14709  tgidm  14788  tgrest  14883  ssidcn  14924  txcnmpt  14987  txcn  14989  blres  15148  mopnval  15156  remetdval  15261  expcn  15283  divccncfap  15304  cncfmet  15306  cncfcncntop  15307  hovergt0  15364  cnplimcim  15381  cnplimclemr  15383  limccnpcntop  15389  limccnp2cntop  15391  dvexp  15425  dvmptid  15430  dvmptfsum  15439  elply2  15449  elplyd  15455  plyaddlem1  15461  plymullem1  15462  plycjlemc  15474  sin0pilem1  15495  pilem3  15497  ef2kpi  15520  sin2pim  15527  cos2pim  15528  sinmpi  15529  cosmpi  15530  sinppi  15531  cosppi  15532  sinhalfpip  15534  sinhalfpim  15535  coshalfpip  15536  coshalfpim  15537  tangtx  15552  1cxp  15614  ecxp  15615  rplogb1  15662  rpelogb  15663  binom4  15693  0sgm  15699  fsumdvdsmul  15705  1sgmprm  15708  1sgm2ppw  15709  lgslem1  15719  gausslemma2dlem4  15783  lgseisenlem1  15789  lgseisenlem2  15790  lgseisenlem3  15791  lgseisenlem4  15792  lgseisen  15793  lgsquadlem1  15796  lgsquadlem2  15797  lgsquadlem3  15798  lgsquad2lem1  15800  m1lgs  15804  2lgslem3a  15812  2lgslem3b  15813  2lgslem3c  15814  2lgslem3d  15815  2sqlem8  15842  opvtxov  15864  opiedgov  15867  structiedg0val  15881  edgov  15904  edg0iedg0g  15907  upgredg  15983  usgrf1oedg  16044  ushgredgedg  16065  ushgredgedgloop  16067  griedg0ssusgr  16090  vtxdgfval  16094  vtxdfifiun  16103  vtxdumgrfival  16104  vtxd0nedgbfi  16105  upgriswlkdc  16157  wlkres  16174  trlreslem  16184  clwwlkn2  16216  ex-ceil  16258  qdencn  16567  cvgcmp2nlemabs  16572  trilpolemlt1  16581  nconstwlpolem0  16603