Theorem eqtr4d 2267

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 2237	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eqtrd 2264	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  3eqtr2d  2270  3eqtr2rd  2271  3eqtr4d  2274  3eqtr4rd  2275  3eqtr4a  2290  sbnfc2  3188  ifsbdc  3618  ifeq1dadc  3636  ifeq2dadc  3637  eqifdc  3642  ifnotdc  3644  2if2dc  3645  ifandc  3646  ifordc  3647  onsucuni2  4662  relop  4880  riinint  4993  iotauni  5299  fniinfv  5704  fsn2  5821  fmptapd  5845  fconst2g  5869  fniunfv  5903  ofres  6250  ofco  6254  caofid1  6264  caofid2  6265  frecsuclem  6572  frecrdg  6574  oasuc  6632  nnacom  6652  nnaass  6653  nndi  6654  nnmass  6655  nnmsucr  6656  nnmcom  6657  funresdfunsndc  6674  uniqs2  6764  en1bg  6974  fundmen  6981  1dom1el  6993  1domsn  7001  pw2f1odclem  7020  mapxpen  7034  xpmapenlem  7035  phplem4dom  7048  en2eqpr  7099  sbthlemi5  7160  omp1eomlem  7293  difinfsnlem  7298  ctmlemr  7307  ctssdccl  7310  ctssdc  7312  infnninf  7323  infnninfOLD  7324  nnnninfeq  7327  pr2cv1  7400  exmidonfinlem  7404  exmidmotap  7480  addcmpblnq  7587  distrnqg  7607  ltexnqq  7628  addcmpblnq0  7663  nqnq0a  7674  nqnq0m  7675  nq0m0r  7676  nq0a0  7677  nnanq0  7678  distrnq0  7679  prarloclemlo  7714  prarloclemcalc  7722  genpassl  7744  genpassu  7745  ltsosr  7984  0idsr  7987  1idsr  7988  mulextsr1lem  8000  cnegex  8357  subsub3  8411  subadd4  8423  mulneg12  8576  mulsub  8580  apreap  8767  cru  8782  recextlem1  8831  cju  9141  ofnegsub  9142  halfaddsub  9378  nn0supp  9454  nneo  9583  zeo2  9586  uzin  9789  xaddcom  10096  xaddass  10104  xleaddadd  10122  iccf1o  10239  fzsuc2  10314  fldiv4lem1div2uz2  10567  flqeqceilz  10581  zmod1congr  10604  modqcyc  10622  modqcyc2  10623  modqaddabs  10625  modqmul1  10640  modqaddmulmod  10654  addmodlteq  10661  frec2uzrdg  10672  frecuzrdgsuctlem  10686  seq3val  10723  seqvalcd  10724  seq3fveq2  10738  seqfveq2g  10740  seq3split  10751  seqsplitg  10752  seqf1oglem2a  10781  seqf1oglem2  10783  seqfeq4g  10794  seq3distr  10795  ser0f  10797  expp1  10809  mulexp  10841  mulexpzap  10842  expadd  10844  expaddzap  10846  expmul  10847  expmulzap  10848  expsubap  10850  expdivap  10853  subsq  10909  mulbinom2  10919  binom3  10920  bernneq  10923  modqexp  10929  nn0opthd  10985  faclbnd  11004  faclbnd6  11007  bccmpl  11017  bcp1n  11024  zfz1isolemiso  11104  seq3coll  11107  hashtpglem  11111  ccatsymb  11183  ccatval1lsw  11185  ccatass  11189  eqs1  11209  lswccats1fst  11225  swrdsb0eq  11250  swrdsbslen  11251  swrds1  11253  ccatswrd  11255  pfxres  11266  ccatpfx  11286  pfxpfx  11293  cats1un  11306  swrdccatin1  11310  pfxccatin12  11318  swrdccat  11320  pfxccat3a  11323  swrdccat3b  11325  shftval2  11391  shftval4  11393  seq3shft  11403  crre  11422  remim  11425  remullem  11436  cjexp  11458  cnrecnv  11475  resqrexlemlo  11578  resqrexlemcalc1  11579  resqrexlemcalc2  11580  resqrexlemcalc3  11581  resqrexlemnm  11583  rsqrmo  11592  abscj  11617  absid  11636  absre  11642  recvalap  11662  maxabsle  11769  maxltsup  11783  2zsupmax  11791  minabs  11801  bdtrilem  11804  bdtri  11805  2zinfmin  11808  xrmaxiflemab  11812  xrmaxiflemcom  11814  xrmaxadd  11826  xrbdtri  11841  iooinsup  11842  climaddc1  11894  climmulc2  11896  climsubc1  11897  climsubc2  11898  climcvg1nlem  11914  summodclem3  11946  zsumdc  11950  isum  11951  isumz  11955  isumss  11957  fisumss  11958  fsum3cvg2  11960  fsumadd  11972  isummulc2  11992  sumsplitdc  11998  fsum2dlemstep  12000  fisumcom2  12004  fisum0diag2  12013  fsumconst  12020  telfsumo  12032  fsumparts  12036  fsumrelem  12037  binomlem  12049  isumshft  12056  isumsplit  12057  arisum  12064  arisum2  12065  trireciplem  12066  geolim2  12078  geo2sum  12080  0.999...  12087  cvgratz  12098  mertensabs  12103  clim2prod  12105  prodf1f  12109  prodmodclem2a  12142  zproddc  12145  iprodap  12146  iprodap0  12148  fprodseq  12149  prod1dc  12152  prodssdc  12155  fprod2dlemstep  12188  fprodcom2fi  12192  fproddivap  12196  ef0lem  12226  efval2  12231  ege2le3  12237  efaddlem  12240  efsub  12247  eftlub  12256  efsep  12257  tanval3ap  12280  efi4p  12283  sinneg  12292  sinmul  12310  sincossq  12314  cos2t  12316  demoivreALT  12340  eirraplem  12343  dvdsmodexp  12361  odd2np1  12439  omoe  12462  divalglemex  12488  divalglemeuneg  12489  divalgmod  12493  flodddiv4  12502  bitsp1  12517  bitsinv1lem  12527  bitsinv1  12528  gcdneg  12558  gcdaddm  12560  modgcd  12567  bezoutlemnewy  12572  gcdass  12591  gcdmultiple  12596  nninfctlemfo  12616  algrp1  12623  lcmneg  12651  lcmgcdeq  12660  lcmass  12662  cncongr2  12681  prmexpb  12728  sqrt2irr  12739  2sqpwodd  12753  qnumdenbi  12769  phiprmpw  12799  eulerthlema  12807  fermltl  12811  prmdiveq  12813  modprm0  12832  pythagtriplem1  12843  pythagtriplem12  12853  pythagtriplem14  12855  pythagtriplem15  12856  pythagtriplem16  12857  pythagtriplem17  12858  pythagtriplem19  12860  pcpremul  12871  pcneg  12903  pcgcd  12907  pc2dvds  12908  pcaddlem  12917  pcprod  12924  fldivp1  12926  pcbc  12929  prmpwdvds  12933  pockthlem  12934  mul4sqlem  12971  4sqlem11  12979  4sqlem12  12980  4sqlem17  12985  ctiunctlemfo  13065  ressval3d  13160  resseqnbasd  13161  prdsval  13361  imasival  13394  qusval  13411  plusfeqg  13452  sgrp1  13499  idmhm  13557  resmhm2  13576  mhmeql  13580  grppropstrg  13607  grpinvinv  13655  grp1  13694  imasgrp2  13702  mulgnngsum  13719  mulginvcom  13739  mulgnndir  13743  mulgdir  13746  mulgneg2  13748  mulgnnass  13749  mulgass  13751  mulgsubdir  13754  trivsubgd  13792  nmzsubg  13802  qussub  13829  idghm  13851  ablinvadd  13902  ablsub2inv  13903  eqgabl  13922  mgpplusgg  13943  mgpbasg  13945  mgpscag  13946  mgptsetg  13947  mgpdsg  13949  mgpress  13950  srgpcomp  14009  srgpcompp  14010  ringo2times  14047  ring1eq0  14067  ring1  14078  opprmulfvalg  14089  crngoppr  14091  opprsllem  14093  oppr1g  14101  opprunitd  14130  rdivmuldivd  14164  rhmunitinv  14198  scafeqg  14328  lmodvsubval2  14362  lmodsubdi  14364  rmodislmod  14371  sralemg  14458  sraipg  14464  crng2idl  14551  cnfldmulg  14596  cnfldexp  14597  cnfldui  14609  mulgrhm2  14630  zrhrhmb  14642  zlmvscag  14653  znval2  14658  znbaslemnn  14659  znunit  14679  psrval  14686  psrgrp  14705  psrneg  14707  mplval2g  14715  restuni2  14907  lmfval  14923  cnfval  14924  cnpfval  14925  txtopon  14992  txcnp  15001  upxp  15002  txrest  15006  cnmptcom  15028  bl2in  15133  xblss2  15135  isxms2  15182  setsmsdsg  15210  setsmstsetg  15211  metss  15224  resubmet  15286  expcn  15299  cncfcncntop  15323  dvidlemap  15421  dvidrelem  15422  dvidsslem  15423  dvcnp2cntop  15429  dvcoapbr  15437  dvcjbr  15438  dvexp  15441  dvexp2  15442  dvrecap  15443  plyaddlem1  15477  plymullem1  15478  plycolemc  15488  plycjlemc  15490  dvply1  15495  efimpi  15549  tangtx  15568  logdivlti  15611  cxpexprp  15625  rpcxpsub  15638  rpabscxpbnd  15670  rprelogbdiv  15687  binom4  15709  mpodvdsmulf1o  15720  0sgmppw  15723  lgslem1  15735  lgsmod  15761  lgsdilem  15762  lgsdi  15772  lgsne0  15773  lgsdirnn0  15782  lgsdinn0  15783  lgseisenlem2  15806  lgseisenlem3  15807  lgsquadlem2  15813  lgsquadlem3  15814  lgsquad2lem1  15816  lgsquad3  15819  2lgslem3  15836  2lgsoddprmlem2  15841  2sqlem4  15853  basvtxval2dom  15891  edgfiedgval2dom  15892  setsvtx  15908  ushgredgedgloop  16085  usgr1vr  16105  wlkres  16236  clwwlkccatlem  16257  trlsegvdegfi  16324  eupth2lem3lem2fi  16326  eupth2lem3lem6fi  16328  eupth2lem3lem4fi  16330  depindlem3  16353  bj-charfundcALT  16430  pw1ndom3lem  16614  pw1ndom3  16615  2omap  16620  sssneq  16629  0nninf  16632  nnnninfex  16650  nninfnfiinf  16651  trilpolemisumle  16668  qdiff  16679  gsumgfsum  16711  gfsump1  16713