Theorem eqtr4d 2265

Description: An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)

Hypotheses

Ref	Expression
eqtr4d.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqtr4d.2	⊢ (𝜑 → 𝐶 = 𝐵)

Assertion

Ref	Expression
eqtr4d	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem eqtr4d

Step	Hyp	Ref	Expression
1		eqtr4d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqtr4d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2235	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 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:  3eqtr2d  2268  3eqtr2rd  2269  3eqtr4d  2272  3eqtr4rd  2273  3eqtr4a  2288  sbnfc2  3185  ifsbdc  3615  ifeq1dadc  3633  ifeq2dadc  3634  eqifdc  3639  ifnotdc  3641  2if2dc  3642  ifandc  3643  ifordc  3644  onsucuni2  4656  relop  4872  riinint  4985  iotauni  5291  fniinfv  5694  fsn2  5811  fmptapd  5834  fconst2g  5858  fniunfv  5892  ofres  6239  ofco  6243  caofid1  6253  caofid2  6254  frecsuclem  6558  frecrdg  6560  oasuc  6618  nnacom  6638  nnaass  6639  nndi  6640  nnmass  6641  nnmsucr  6642  nnmcom  6643  funresdfunsndc  6660  uniqs2  6750  en1bg  6960  fundmen  6967  1domsn  6984  pw2f1odclem  7003  mapxpen  7017  xpmapenlem  7018  phplem4dom  7031  en2eqpr  7080  sbthlemi5  7139  omp1eomlem  7272  difinfsnlem  7277  ctmlemr  7286  ctssdccl  7289  ctssdc  7291  infnninf  7302  infnninfOLD  7303  nnnninfeq  7306  pr2cv1  7379  exmidonfinlem  7382  exmidmotap  7458  addcmpblnq  7565  distrnqg  7585  ltexnqq  7606  addcmpblnq0  7641  nqnq0a  7652  nqnq0m  7653  nq0m0r  7654  nq0a0  7655  nnanq0  7656  distrnq0  7657  prarloclemlo  7692  prarloclemcalc  7700  genpassl  7722  genpassu  7723  ltsosr  7962  0idsr  7965  1idsr  7966  mulextsr1lem  7978  cnegex  8335  subsub3  8389  subadd4  8401  mulneg12  8554  mulsub  8558  apreap  8745  cru  8760  recextlem1  8809  cju  9119  ofnegsub  9120  halfaddsub  9356  nn0supp  9432  nneo  9561  zeo2  9564  uzin  9767  xaddcom  10069  xaddass  10077  xleaddadd  10095  iccf1o  10212  fzsuc2  10287  fldiv4lem1div2uz2  10538  flqeqceilz  10552  zmod1congr  10575  modqcyc  10593  modqcyc2  10594  modqaddabs  10596  modqmul1  10611  modqaddmulmod  10625  addmodlteq  10632  frec2uzrdg  10643  frecuzrdgsuctlem  10657  seq3val  10694  seqvalcd  10695  seq3fveq2  10709  seqfveq2g  10711  seq3split  10722  seqsplitg  10723  seqf1oglem2a  10752  seqf1oglem2  10754  seqfeq4g  10765  seq3distr  10766  ser0f  10768  expp1  10780  mulexp  10812  mulexpzap  10813  expadd  10815  expaddzap  10817  expmul  10818  expmulzap  10819  expsubap  10821  expdivap  10824  subsq  10880  mulbinom2  10890  binom3  10891  bernneq  10894  modqexp  10900  nn0opthd  10956  faclbnd  10975  faclbnd6  10978  bccmpl  10988  bcp1n  10995  zfz1isolemiso  11074  seq3coll  11077  ccatsymb  11150  ccatval1lsw  11152  ccatass  11156  eqs1  11176  lswccats1fst  11190  swrdsb0eq  11212  swrdsbslen  11213  swrds1  11215  ccatswrd  11217  pfxres  11228  ccatpfx  11248  pfxpfx  11255  cats1un  11268  swrdccatin1  11272  pfxccatin12  11280  swrdccat  11282  pfxccat3a  11285  swrdccat3b  11287  shftval2  11352  shftval4  11354  seq3shft  11364  crre  11383  remim  11386  remullem  11397  cjexp  11419  cnrecnv  11436  resqrexlemlo  11539  resqrexlemcalc1  11540  resqrexlemcalc2  11541  resqrexlemcalc3  11542  resqrexlemnm  11544  rsqrmo  11553  abscj  11578  absid  11597  absre  11603  recvalap  11623  maxabsle  11730  maxltsup  11744  2zsupmax  11752  minabs  11762  bdtrilem  11765  bdtri  11766  2zinfmin  11769  xrmaxiflemab  11773  xrmaxiflemcom  11775  xrmaxadd  11787  xrbdtri  11802  iooinsup  11803  climaddc1  11855  climmulc2  11857  climsubc1  11858  climsubc2  11859  climcvg1nlem  11875  summodclem3  11906  zsumdc  11910  isum  11911  isumz  11915  isumss  11917  fisumss  11918  fsum3cvg2  11920  fsumadd  11932  isummulc2  11952  sumsplitdc  11958  fsum2dlemstep  11960  fisumcom2  11964  fisum0diag2  11973  fsumconst  11980  telfsumo  11992  fsumparts  11996  fsumrelem  11997  binomlem  12009  isumshft  12016  isumsplit  12017  arisum  12024  arisum2  12025  trireciplem  12026  geolim2  12038  geo2sum  12040  0.999...  12047  cvgratz  12058  mertensabs  12063  clim2prod  12065  prodf1f  12069  prodmodclem2a  12102  zproddc  12105  iprodap  12106  iprodap0  12108  fprodseq  12109  prod1dc  12112  prodssdc  12115  fprod2dlemstep  12148  fprodcom2fi  12152  fproddivap  12156  ef0lem  12186  efval2  12191  ege2le3  12197  efaddlem  12200  efsub  12207  eftlub  12216  efsep  12217  tanval3ap  12240  efi4p  12243  sinneg  12252  sinmul  12270  sincossq  12274  cos2t  12276  demoivreALT  12300  eirraplem  12303  dvdsmodexp  12321  odd2np1  12399  omoe  12422  divalglemex  12448  divalglemeuneg  12449  divalgmod  12453  flodddiv4  12462  bitsp1  12477  bitsinv1lem  12487  bitsinv1  12488  gcdneg  12518  gcdaddm  12520  modgcd  12527  bezoutlemnewy  12532  gcdass  12551  gcdmultiple  12556  nninfctlemfo  12576  algrp1  12583  lcmneg  12611  lcmgcdeq  12620  lcmass  12622  cncongr2  12641  prmexpb  12688  sqrt2irr  12699  2sqpwodd  12713  qnumdenbi  12729  phiprmpw  12759  eulerthlema  12767  fermltl  12771  prmdiveq  12773  modprm0  12792  pythagtriplem1  12803  pythagtriplem12  12813  pythagtriplem14  12815  pythagtriplem15  12816  pythagtriplem16  12817  pythagtriplem17  12818  pythagtriplem19  12820  pcpremul  12831  pcneg  12863  pcgcd  12867  pc2dvds  12868  pcaddlem  12877  pcprod  12884  fldivp1  12886  pcbc  12889  prmpwdvds  12893  pockthlem  12894  mul4sqlem  12931  4sqlem11  12939  4sqlem12  12940  4sqlem17  12945  ctiunctlemfo  13025  ressval3d  13120  resseqnbasd  13121  prdsval  13321  imasival  13354  qusval  13371  plusfeqg  13412  sgrp1  13459  idmhm  13517  resmhm2  13536  mhmeql  13540  grppropstrg  13567  grpinvinv  13615  grp1  13654  imasgrp2  13662  mulgnngsum  13679  mulginvcom  13699  mulgnndir  13703  mulgdir  13706  mulgneg2  13708  mulgnnass  13709  mulgass  13711  mulgsubdir  13714  trivsubgd  13752  nmzsubg  13762  qussub  13789  idghm  13811  ablinvadd  13862  ablsub2inv  13863  eqgabl  13882  mgpplusgg  13902  mgpbasg  13904  mgpscag  13905  mgptsetg  13906  mgpdsg  13908  mgpress  13909  srgpcomp  13968  srgpcompp  13969  ringo2times  14006  ring1eq0  14026  ring1  14037  opprmulfvalg  14048  crngoppr  14050  opprsllem  14052  oppr1g  14060  opprunitd  14089  rdivmuldivd  14123  rhmunitinv  14157  scafeqg  14287  lmodvsubval2  14321  lmodsubdi  14323  rmodislmod  14330  sralemg  14417  sraipg  14423  crng2idl  14510  cnfldmulg  14555  cnfldexp  14556  cnfldui  14568  mulgrhm2  14589  zrhrhmb  14601  zlmvscag  14612  znval2  14617  znbaslemnn  14618  znunit  14638  psrval  14645  psrgrp  14664  psrneg  14666  mplval2g  14674  restuni2  14866  lmfval  14882  cnfval  14883  cnpfval  14884  txtopon  14951  txcnp  14960  upxp  14961  txrest  14965  cnmptcom  14987  bl2in  15092  xblss2  15094  isxms2  15141  setsmsdsg  15169  setsmstsetg  15170  metss  15183  resubmet  15245  expcn  15258  cncfcncntop  15282  dvidlemap  15380  dvidrelem  15381  dvidsslem  15382  dvcnp2cntop  15388  dvcoapbr  15396  dvcjbr  15397  dvexp  15400  dvexp2  15401  dvrecap  15402  plyaddlem1  15436  plymullem1  15437  plycolemc  15447  plycjlemc  15449  dvply1  15454  efimpi  15508  tangtx  15527  logdivlti  15570  cxpexprp  15584  rpcxpsub  15597  rpabscxpbnd  15629  rprelogbdiv  15646  binom4  15668  mpodvdsmulf1o  15679  0sgmppw  15682  lgslem1  15694  lgsmod  15720  lgsdilem  15721  lgsdi  15731  lgsne0  15732  lgsdirnn0  15741  lgsdinn0  15742  lgseisenlem2  15765  lgseisenlem3  15766  lgsquadlem2  15772  lgsquadlem3  15773  lgsquad2lem1  15775  lgsquad3  15778  2lgslem3  15795  2lgsoddprmlem2  15800  2sqlem4  15812  basvtxval2dom  15850  edgfiedgval2dom  15851  setsvtx  15867  ushgredgedgloop  16041  wlkres  16118  clwwlkccatlem  16137  bj-charfundcALT  16227  1dom1el  16409  pw1ndom3lem  16412  pw1ndom3  16413  2omap  16418  sssneq  16427  0nninf  16430  nnnninfex  16448  nninfnfiinf  16449  trilpolemisumle  16466