Theorem eqtrid 2238

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 2226	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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  eqtr2id  2239  eqtr3id  2240  3eqtr3a  2250  3eqtr4g  2251  csbtt  3093  csbvarg  3109  csbie2g  3132  rabbi2dva  3368  csbprc  3493  disjssun  3511  disjpr2  3683  prprc2  3728  difprsn2  3759  opprc  3826  intsng  3905  riinm  3986  iinxsng  3987  iunxprg  3994  rintm  4006  sucprc  4444  unisucg  4446  xpriindim  4801  relop  4813  dmxpm  4883  riinint  4924  resabs1  4972  resabs2  4974  resima2  4977  xpssres  4978  resopab2  4990  mptimass  5019  imasng  5031  ndmima  5043  xpdisj1  5091  xpdisj2  5092  djudisj  5094  resdisj  5095  rnxpm  5096  xpima1  5113  xpima2m  5114  dmsnsnsng  5144  rnsnopg  5145  rnpropg  5146  mptiniseg  5161  dfco2a  5167  relcoi1  5198  unixpm  5202  iotaval  5227  funtp  5308  fnun  5361  fnresdisj  5365  fnima  5373  fnimaeq0  5376  fcoi1  5435  f1orescnv  5517  foun  5520  resdif  5523  tz6.12-2  5546  fveu  5547  tz6.12-1  5582  fvun2  5625  fvopab3ig  5632  f1oresrab  5724  dfmptg  5738  ressnop0  5740  fvunsng  5753  fnsnsplitss  5758  fsnunfv  5760  fvpr1  5763  fvpr2  5764  fvpr1g  5765  fvpr2g  5766  fvtp1g  5767  fvtp2g  5768  fvtp3g  5769  fvtp2  5771  fvtp3  5772  f1oiso2  5871  riotaund  5909  ovprc  5954  resoprab2  6016  fnoprabg  6020  ovidig  6037  ovigg  6040  fvmpopr2d  6056  ov6g  6058  ovconst2  6072  offval2  6148  ot1stg  6207  ot2ndg  6208  ot3rdgg  6209  fmpoco  6271  algrflemg  6285  tpostpos2  6320  rdgisuc1  6439  frec0g  6452  frecsuclem  6461  frecrdg  6463  oasuc  6519  oa1suc  6522  omsuc  6527  nnm1  6580  nnm2  6581  dfec2  6592  errn  6611  ixpsnval  6757  ixpintm  6781  mapen  6904  xpmapenlem  6907  phplem2  6911  undifdc  6982  fisseneq  6990  ssfirab  6992  eqinfti  7081  infvalti  7083  infsnti  7091  casef  7149  caseinl  7152  caseinr  7153  djudom  7154  ctssdccl  7172  nninfwlpoimlemginf  7237  exmidfodomrlemim  7263  1qec  7450  mulidnq  7451  addpinq1  7526  suplocexprlem2b  7776  suplocexprlemlub  7786  0idsr  7829  1idsr  7830  caucvgsrlemoffres  7862  caucvgsr  7864  mulresr  7900  pitonnlem2  7909  ax1rid  7939  axcnre  7943  negid  8268  subneg  8270  negneg  8271  dfinfre  8977  2times  9112  infrenegsupex  9662  rexneg  9899  xaddpnf2  9916  xaddmnf1  9917  xaddmnf2  9918  fseq1p1m1  10163  fzosplitprm1  10304  intfracq  10394  frec2uz0d  10473  frec2uzrdg  10483  frecuzrdg0  10487  frecuzrdgg  10490  frecuzrdg0t  10496  seq3val  10534  seqvalcd  10535  iseqf1olemjpcl  10582  iseqf1olemqpcl  10583  iseqf1olemfvp  10584  seq3f1olemqsum  10587  seqf1oglem2  10594  sqval  10671  iexpcyc  10718  binom3  10731  faclbnd  10815  faclbnd2  10816  bcn1  10832  hashinfom  10852  hashennn  10854  hashxp  10900  csbwrdg  10946  shftlem  10963  shftuz  10964  shftidt  10980  reim0  11008  remullem  11018  resqrexlemf1  11155  resqrexlemcalc3  11163  absexpzap  11227  absimle  11231  amgm2  11265  minmax  11376  mingeb  11388  2zinfmin  11389  xrmaxiflemval  11396  xrmaxadd  11407  infxrnegsupex  11409  xrminmax  11411  summodc  11529  fsum3  11533  sumsnf  11555  sumsns  11561  isumclim3  11569  isumge0  11576  fsump1i  11579  fsum2dlemstep  11580  fisumcom2  11584  fsumshftm  11591  fsumconst  11600  fsumiun  11623  hashrabrex  11627  hashuni  11628  binom11  11632  isumsplit  11637  geo2sum  11660  mertensabs  11683  prodmodc  11724  fprodseq  11729  prodsnf  11738  prodsns  11749  fprodconst  11766  fprod2dlemstep  11768  fprodcom2fi  11772  efgt1p2  11841  efgt1p  11842  resinval  11861  recosval  11862  cosadd  11883  ef01bndlem  11902  eirraplem  11923  nninfctlemfo  12180  ialgr0  12185  algrp1  12187  eucalg  12200  phiprmpw  12363  phiprm  12364  prmdiv  12376  pythagtriplem12  12416  pythagtriplem14  12418  pythagtriplem16  12420  pceu  12436  pcfac  12491  prmpwdvds  12496  4sqlem5  12523  mul4sqlem  12534  ennnfonelem0  12565  ennnfonelemfun  12577  ennnfonelemf1  12578  ennnfonelemrn  12579  ctinfomlemom  12587  nninfdclemp1  12610  ndxid  12645  setsfun0  12657  setsresg  12659  setscom  12661  strslfv2d  12664  basm  12682  ressval3d  12693  resseqnbasd  12694  imasaddvallemg  12901  xpsval  12938  plusffvalg  12948  mgm1  12956  grpidvalg  12959  sgrp1  12997  mnd1  13030  mnd1id  13031  subsubm  13058  grppropstrg  13094  grpinvfvalg  13117  grpsubfvalg  13120  grp1  13181  mulgfvalg  13194  mulgnn0gsum  13201  mulg2  13204  subsubg  13270  releqgg  13293  eqgfval  13295  conjsubg  13350  gsumfzconstf  13415  mgpvalg  13422  mgpbasg  13425  mgpscag  13426  mgptopng  13428  mgpdsg  13429  mgpress  13430  ringidvalg  13460  ring1  13558  opprvalg  13568  opprmulfvalg  13569  opprbasg  13574  oppraddg  13575  subsubrng  13713  subsubrg  13744  rrgval  13761  scaffvalg  13805  lmodpropd  13848  lsssetm  13855  lsslss  13880  lspfval  13887  sraring  13948  lidlvalg  13970  rspvalg  13971  lidlss  13975  islidlm  13978  lidl0cl  13982  lidlacl  13983  lidlnegcl  13984  lidl0  13988  lidl1  13989  rspcl  13990  rspssid  13991  rsp0  13992  rspssp  13993  2idlval  14001  2idlvalg  14002  crngridl  14029  rspsn  14033  zrhval  14116  zrhvalg  14117  zlmval  14126  zlmbasg  14128  zlmplusgg  14129  zlmmulrg  14130  znval  14135  znzrh2  14145  znf1o  14150  psrval  14163  tgidm  14253  tgrest  14348  ssidcn  14389  txcnmpt  14452  txcn  14454  blres  14613  mopnval  14621  remetdval  14726  expcn  14748  divccncfap  14769  cncfmet  14771  cncfcncntop  14772  hovergt0  14829  cnplimcim  14846  cnplimclemr  14848  limccnpcntop  14854  limccnp2cntop  14856  dvexp  14890  dvmptid  14895  dvmptfsum  14904  elply2  14914  elplyd  14920  plyaddlem1  14926  plymullem1  14927  plycjlemc  14938  sin0pilem1  14957  pilem3  14959  ef2kpi  14982  sin2pim  14989  cos2pim  14990  sinmpi  14991  cosmpi  14992  sinppi  14993  cosppi  14994  sinhalfpip  14996  sinhalfpim  14997  coshalfpip  14998  coshalfpim  14999  tangtx  15014  1cxp  15076  ecxp  15077  rplogb1  15121  rpelogb  15122  binom4  15152  lgslem1  15157  gausslemma2dlem4  15221  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem3  15229  lgseisenlem4  15230  lgseisen  15231  lgsquadlem1  15234  lgsquadlem2  15235  lgsquadlem3  15236  lgsquad2lem1  15238  m1lgs  15242  2lgslem3a  15250  2lgslem3b  15251  2lgslem3c  15252  2lgslem3d  15253  2sqlem8  15280  ex-ceil  15288  qdencn  15587  cvgcmp2nlemabs  15592  trilpolemlt1  15601  nconstwlpolem0  15623