Theorem eqtrid 2283

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqtr2id  2284  eqtr3id  2285  3eqtr3a  2295  3eqtr4g  2296  eqab  2373  csbtt  3159  csbvarg  3175  csbie2g  3198  rabbi2dva  3439  csbprc  3572  disjssun  3588  inssdif0im  3592  disjpr2  3773  rabsnif  3778  prprc2  3822  difprsn2  3855  opprc  3925  intsng  4004  riinm  4085  iinxsng  4086  iunxprg  4093  rintm  4105  sucprc  4557  unisucg  4559  xpriindim  4918  relop  4930  dmxpm  5002  riinint  5043  resabs1  5092  resabs2  5094  resima2  5097  xpssres  5098  resopab2  5110  mptimass  5139  imasng  5152  ndmima  5164  xpdisj1  5212  xpdisj2  5213  djudisj  5215  resdisj  5216  rnxpm  5217  xpima1  5234  xpima2m  5235  dmsnsnsng  5265  rnsnopg  5266  rnpropg  5267  mptiniseg  5282  dfco2a  5288  relcoi1  5319  unixpm  5323  iotaval  5349  funtp  5434  fnun  5489  fnresdisj  5493  fnima  5502  fnimaeq0  5505  fresaunres2disj  5570  fcoi1  5572  f1orescnv  5655  foun  5658  resdif  5661  tz6.12-2  5686  fveu  5687  tz6.12-1  5722  fvun2  5770  fvopab3ig  5779  f1oresrab  5873  dfmptg  5888  funopsn  5891  ressnop0  5896  fvunsng  5909  fnsnsplitss  5914  fsnunfv  5916  fvpr1  5919  fvpr2  5920  fvpr1g  5921  fvpr2g  5922  fvtp1g  5923  fvtp2g  5924  fvtp3g  5925  fvtp2  5927  fvtp3  5928  f1oiso2  6033  riotaund  6075  ovprc  6121  resoprab2  6185  fnoprabg  6189  ovidig  6206  ovigg  6209  fvmpopr2d  6225  ov6g  6227  ovconst2  6241  offval2  6318  ot1stg  6386  ot2ndg  6387  ot3rdgg  6388  opabn1stprc  6429  fmpoco  6452  algrflemg  6466  suppsnopdc  6490  tpostpos2  6536  rdgisuc1  6655  frec0g  6668  frecsuclem  6677  frecrdg  6679  oasuc  6737  oa1suc  6740  omsuc  6745  nnm1  6798  nnm2  6799  dfec2  6810  errn  6829  ixpsnval  6983  ixpintm  7007  mapen  7146  xpmapenlem  7149  phplem2  7154  undifdc  7231  prfidceq  7235  fisseneq  7242  ssfirab  7244  eqinfti  7361  infvalti  7363  infsnti  7371  casef  7429  caseinl  7432  caseinr  7433  djudom  7434  ctssdccl  7452  nninfwlpoimlemginf  7517  exmidfodomrlemim  7554  1qec  7756  mulidnq  7757  addpinq1  7832  suplocexprlem2b  8082  suplocexprlemlub  8092  0idsr  8135  1idsr  8136  caucvgsrlemoffres  8168  caucvgsr  8170  mulresr  8206  pitonnlem2  8215  ax1rid  8245  axcnre  8249  negid  8575  subneg  8577  negneg  8578  dfinfre  9289  2times  9435  infrenegsupex  10004  rexneg  10243  xaddpnf2  10260  xaddmnf1  10261  xaddmnf2  10262  fseq1p1m1  10512  fzosplitprm1  10664  infssfzcldc  10680  infssfzledc  10681  intfracq  10772  frec2uz0d  10851  frec2uzrdg  10861  frecuzrdg0  10865  frecuzrdgg  10868  frecuzrdg0t  10874  seq3val  10912  seqvalcd  10913  iseqf1olemjpcl  10960  iseqf1olemqpcl  10961  iseqf1olemfvp  10962  seq3f1olemqsum  10965  seqf1oglem2  10972  sqval  11049  iexpcyc  11096  binom3  11109  faclbnd  11195  faclbnd2  11196  bcn1  11212  hashinfom  11233  hashennn  11235  hashxp  11283  hashfibclem  11298  hashfibc  11299  hashf1lem1  11301  hashf1lem2  11302  hashtpgim  11313  hashtpglem  11314  hashtpg  11315  csbwrdg  11350  ccatlid  11390  s1val  11401  swrd00g  11437  pfxclz  11467  pfxccatpfx2  11525  cats1fvn  11552  cats1fvd  11554  cats1lend  11555  shftlem  11597  shftuz  11598  shftidt  11614  reim0  11642  remullem  11652  resqrexlemf1  11790  resqrexlemcalc3  11798  absexpzap  11863  absimle  11867  amgm2  11901  minmax  12014  mingeb  12027  2zinfmin  12028  xrmaxiflemval  12035  xrmaxadd  12046  infxrnegsupex  12048  xrminmax  12050  summodc  12169  fsum3  12173  sumsnf  12195  sumsns  12201  isumclim3  12209  isumge0  12216  fsump1i  12219  fsum2dlemstep  12220  fisumcom2  12224  fsumshftm  12231  fsumconst  12240  fsumiun  12263  hashrabrex  12267  hashuni  12268  binom11  12272  isumsplit  12277  geo2sum  12300  mertensabs  12323  prodmodc  12364  fprodseq  12369  prodsnf  12378  prodsns  12389  fprodconst  12406  fprod2dlemstep  12408  fprodcom2fi  12412  efgt1p2  12481  efgt1p  12482  resinval  12501  recosval  12502  cosadd  12523  ef01bndlem  12542  eirraplem  12563  bits0  12734  nninfctlemfo  12836  ialgr0  12841  algrp1  12843  eucalg  12856  phiprmpw  13023  phiprm  13024  prmdiv  13036  pythagtriplem12  13077  pythagtriplem14  13079  pythagtriplem16  13081  pceu  13097  pcfac  13152  prmpwdvds  13157  4sqlem5  13184  mul4sqlem  13195  ballotfilem4  13293  ballotfilem1c  13303  ballotfilemgun  13320  ennnfonelem0  13348  ennnfonelemfun  13360  ennnfonelemf1  13361  ennnfonelemrn  13362  ctinfomlemom  13370  nninfdclemp1  13393  ndxid  13428  setsfun0  13440  setsresg  13442  setscom  13444  strslfv2d  13447  basm  13466  ressval3d  13479  resseqnbasd  13480  imasaddvallemg  13689  plusffvalg  13735  mgm1  13743  grpidvalg  13746  sgrp1  13779  mnd1  13815  mnd1id  13816  subsubm  13843  grppropstrg  13877  grpinvfvalg  13900  grpsubfvalg  13903  grp1  13964  mulgfvalg  13977  mulgnn0gzsum  13984  mulg2  13987  subsubg  14053  releqgg  14076  eqgfval  14078  conjsubg  14133  cntzfval  14146  gzsumconstf  14228  gsump1  14241  gsumclfi  14243  gsummptfidmadd  14245  gsumconstcmn  14250  prdsval  14257  prdsidlem  14277  prdsinvlem  14280  xpsval  14285  pwsval  14288  pwsplusgval  14292  pwsmulrval  14293  pwsinvg  14299  mgpvalg  14304  mgpbasg  14308  mgpscag  14310  mgptopng  14312  mgpdsg  14313  mgpress  14314  ringidvalg  14348  ring1  14448  opprvalg  14458  opprmulfvalg  14459  opprbasg  14464  oppraddg  14465  subsubrng  14606  subsubrg  14637  rrgval  14654  scaffvalg  14727  lmodpropd  14770  lsssetm  14777  lsslss  14802  lspfval  14809  sraring  14870  lidlvalg  14892  rspvalg  14893  lidlss  14897  islidlm  14900  lidl0cl  14904  lidlacl  14905  lidlnegcl  14906  lidl0  14910  lidl1  14911  rspcl  14912  rspssid  14913  rsp0  14914  rspssp  14915  2idlval  14923  2idlvalg  14924  crngridl  14951  rspsn  14955  zrhval  15036  zrhvalg  15037  zlmval  15046  zlmbasg  15048  zlmplusgg  15049  zlmmulrg  15050  znval  15055  znzrh2  15065  znf1o  15070  assapropd  15098  aspval  15099  psrval  15134  mplvalcoe  15172  mpl0fi  15184  mplnegfi  15187  tgidm  15266  tgrest  15361  ssidcn  15402  txcnmpt  15465  txcn  15467  blres  15626  mopnval  15634  remetdval  15739  expcn  15761  divccncfap  15782  cncfmet  15784  cncfcncntop  15785  hovergt0  15842  cnplimcim  15859  cnplimclemr  15861  limccnpcntop  15867  limccnp2cntop  15869  dvexp  15903  dvmptid  15908  dvmptfsum  15917  elply2  15927  elplyd  15933  plyaddlem1  15939  plymullem1  15940  plycjlemc  15952  sin0pilem1  15974  pilem3  15976  ef2kpi  15999  sin2pim  16006  cos2pim  16007  sinmpi  16008  cosmpi  16009  sinppi  16010  cosppi  16011  sinhalfpip  16013  sinhalfpim  16014  coshalfpip  16015  coshalfpim  16016  tangtx  16031  1cxp  16097  ecxp  16098  rplogb1  16145  rpelogb  16146  zprmlogbaplem2  16177  binom4  16180  log2tlbndlog2  16181  birthdaylem2  16187  birthdaylem3  16188  0sgm  16215  fsumdvdsmul  16246  1sgmprm  16249  1sgm2ppw  16250  ppiqub  16254  chtqub  16257  bposlem9  16280  lgslem1  16285  gausslemma2dlem4  16349  lgseisenlem1  16355  lgseisenlem2  16356  lgseisenlem3  16357  lgseisenlem4  16358  lgseisen  16359  lgsquadlem1  16362  lgsquadlem2  16363  lgsquadlem3  16364  lgsquad2lem1  16366  m1lgs  16370  2lgslem3a  16378  2lgslem3b  16379  2lgslem3c  16380  2lgslem3d  16381  2sqlem8  16408  opvtxov  16430  opiedgov  16433  structiedg0val  16447  edgov  16470  edg0iedg0g  16473  upgredg  16551  usgrf1oedg  16612  ushgredgedg  16633  ushgredgedgloop  16635  griedg0ssusgr  16658  subgrprop3  16669  0uhgrsubgr  16672  vtxdgfval  16695  vtxdfifiun  16704  vtxdumgrfival  16705  vtxd0nedgbfi  16706  1hevtxdg1en  16715  upgriswlkdc  16767  wlkres  16786  trlreslem  16796  clwwlkn2  16828  eupthvdres  16882  eupth2lem3fi  16883  ex-ceil  16906  depindlem1  16913  qdencn  17238  cvgcmp2nlemabs  17247  trilpolemlt1  17257  nconstwlpolem0  17280