Theorem eqtr4d 2268

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

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  3eqtr2d  2271  3eqtr2rd  2272  3eqtr4d  2275  3eqtr4rd  2276  3eqtr4a  2291  sbnfc2  3199  ifsbdc  3635  ifeq1dadc  3653  ifeq2dadc  3654  eqifdc  3659  ifnotdc  3661  2if2dc  3662  ifandc  3663  ifordc  3664  onsucuni2  4686  relop  4905  riinint  5018  iotauni  5325  fniinfv  5735  fsn2  5851  fmptapd  5875  fconst2g  5899  fniunfv  5935  ofres  6281  ofco  6285  caofid1  6295  caofid2  6296  fsuppeq  6447  fsuppeqg  6448  frecsuclem  6637  frecrdg  6639  oasuc  6697  nnacom  6717  nnaass  6718  nndi  6719  nnmass  6720  nnmsucr  6721  nnmcom  6722  funresdfunsndc  6739  uniqs2  6829  en1bg  7040  fundmen  7047  1dom1el  7060  1domsn  7068  pw2f1odclem  7087  mapxpen  7101  xpmapenlem  7102  mapunen  7104  phplem4dom  7116  en2eqpr  7167  sbthlemi5  7231  2omap  7269  omp1eomlem  7385  difinfsnlem  7390  ctmlemr  7399  ctssdccl  7402  ctssdc  7404  infnninf  7415  infnninfOLD  7416  nnnninfeq  7419  pr2cv1  7492  exmidonfinlem  7496  exmidmotap  7575  addcmpblnq  7682  distrnqg  7702  ltexnqq  7723  addcmpblnq0  7758  nqnq0a  7769  nqnq0m  7770  nq0m0r  7771  nq0a0  7772  nnanq0  7773  distrnq0  7774  prarloclemlo  7809  prarloclemcalc  7817  genpassl  7839  genpassu  7840  ltsosr  8079  0idsr  8082  1idsr  8083  mulextsr1lem  8095  cnegex  8451  subsub3  8505  subadd4  8517  mulneg12  8670  mulsub  8674  apreap  8861  cru  8876  recextlem1  8925  cju  9235  ofnegsub  9236  halfaddsub  9472  nn0supp  9552  nneo  9681  zeo2  9684  uzin  9887  xaddcom  10194  xaddass  10202  xleaddadd  10220  iccf1o  10338  fzsuc2  10413  fldiv4lem1div2uz2  10666  flqeqceilz  10680  zmod1congr  10703  modqcyc  10721  modqcyc2  10722  modqaddabs  10724  modqmul1  10739  modqaddmulmod  10753  addmodlteq  10760  frec2uzrdg  10771  frecuzrdgsuctlem  10785  seq3val  10822  seqvalcd  10823  seq3fveq2  10837  seqfveq2g  10839  seq3split  10850  seqsplitg  10851  seqf1oglem2a  10880  seqf1oglem2  10882  seqfeq4g  10893  seq3distr  10894  ser0f  10896  expp1  10908  mulexp  10940  mulexpzap  10941  expadd  10943  expaddzap  10945  expmul  10946  expmulzap  10947  expsubap  10949  expdivap  10952  subsq  11008  mulbinom2  11018  binom3  11019  bernneq  11022  modqexp  11028  nn0opthd  11084  faclbnd  11103  faclbnd6  11106  bccmpl  11116  bcp1n  11123  hashfibclem  11206  hashfibc  11207  zfz1isolemiso  11211  seq3coll  11214  hashtpglem  11218  ccatsymb  11290  ccatval1lsw  11292  ccatass  11296  eqs1  11316  lswccats1fst  11332  swrdsb0eq  11357  swrdsbslen  11358  swrds1  11360  ccatswrd  11362  pfxres  11373  ccatpfx  11393  pfxpfx  11400  cats1un  11413  swrdccatin1  11417  pfxccatin12  11425  swrdccat  11427  pfxccat3a  11430  swrdccat3b  11432  shftval2  11511  shftval4  11513  seq3shft  11523  crre  11542  remim  11545  remullem  11556  cjexp  11578  cnrecnv  11595  resqrexlemlo  11698  resqrexlemcalc1  11699  resqrexlemcalc2  11700  resqrexlemcalc3  11701  resqrexlemnm  11703  rsqrmo  11712  abscj  11737  absid  11756  absre  11762  recvalap  11782  maxabsle  11889  maxltsup  11903  2zsupmax  11911  minabs  11921  bdtrilem  11924  bdtri  11925  2zinfmin  11928  xrmaxiflemab  11932  xrmaxiflemcom  11934  xrmaxadd  11946  xrbdtri  11961  iooinsup  11962  climaddc1  12014  climmulc2  12016  climsubc1  12017  climsubc2  12018  climcvg1nlem  12034  summodclem3  12066  zsumdc  12070  isum  12071  isumz  12075  isumss  12077  fisumss  12078  fsum3cvg2  12080  fsumadd  12092  isummulc2  12112  sumsplitdc  12118  fsum2dlemstep  12120  fisumcom2  12124  fisum0diag2  12133  fsumconst  12140  telfsumo  12152  fsumparts  12156  fsumrelem  12157  binomlem  12169  isumshft  12176  isumsplit  12177  arisum  12184  arisum2  12185  trireciplem  12186  geolim2  12198  geo2sum  12200  0.999...  12207  cvgratz  12218  mertensabs  12223  clim2prod  12225  prodf1f  12229  prodmodclem2a  12262  zproddc  12265  iprodap  12266  iprodap0  12268  fprodseq  12269  prod1dc  12272  prodssdc  12275  fprod2dlemstep  12308  fprodcom2fi  12312  fproddivap  12316  ef0lem  12346  efval2  12351  ege2le3  12357  efaddlem  12360  efsub  12367  eftlub  12376  efsep  12377  tanval3ap  12400  efi4p  12403  sinneg  12412  sinmul  12430  sincossq  12434  cos2t  12436  demoivreALT  12460  eirraplem  12463  dvdsmodexp  12481  odd2np1  12559  omoe  12582  divalglemex  12608  divalglemeuneg  12609  divalgmod  12613  flodddiv4  12622  bitsp1  12637  bitsinv1lem  12647  bitsinv1  12648  gcdneg  12678  gcdaddm  12680  modgcd  12687  bezoutlemnewy  12692  gcdass  12711  gcdmultiple  12716  nninfctlemfo  12736  algrp1  12743  lcmneg  12771  lcmgcdeq  12780  lcmass  12782  cncongr2  12801  prmexpb  12848  sqrt2irr  12859  2sqpwodd  12873  qnumdenbi  12889  phiprmpw  12919  eulerthlema  12927  fermltl  12931  prmdiveq  12933  modprm0  12952  pythagtriplem1  12963  pythagtriplem12  12973  pythagtriplem14  12975  pythagtriplem15  12976  pythagtriplem16  12977  pythagtriplem17  12978  pythagtriplem19  12980  pcpremul  12991  pcneg  13023  pcgcd  13027  pc2dvds  13028  pcaddlem  13037  pcprod  13044  fldivp1  13046  pcbc  13049  prmpwdvds  13053  pockthlem  13054  mul4sqlem  13091  4sqlem11  13099  4sqlem12  13100  4sqlem17  13105  ctiunctlemfo  13190  ressval3d  13285  resseqnbasd  13286  prdsval  13486  imasival  13519  qusval  13536  plusfeqg  13577  sgrp1  13624  idmhm  13682  resmhm2  13701  mhmeql  13705  grppropstrg  13732  grpinvinv  13780  grp1  13819  imasgrp2  13827  mulgnngsum  13844  mulginvcom  13864  mulgnndir  13868  mulgdir  13871  mulgneg2  13873  mulgnnass  13874  mulgass  13876  mulgsubdir  13879  trivsubgd  13917  nmzsubg  13927  qussub  13954  idghm  13976  ablinvadd  14027  ablsub2inv  14028  eqgabl  14047  mgpplusgg  14068  mgpbasg  14070  mgpscag  14071  mgptsetg  14072  mgpdsg  14074  mgpress  14075  srgpcomp  14134  srgpcompp  14135  ringo2times  14172  ring1eq0  14192  ring1  14203  opprmulfvalg  14214  crngoppr  14216  opprsllem  14218  oppr1g  14226  opprunitd  14255  rdivmuldivd  14289  rhmunitinv  14323  scafeqg  14456  lmodvsubval2  14490  lmodsubdi  14492  rmodislmod  14499  sralemg  14586  sraipg  14592  crng2idl  14679  cnfldmulg  14724  cnfldexp  14725  cnfldui  14737  mulgrhm2  14758  zrhrhmb  14770  zlmvscag  14781  znval2  14786  znbaslemnn  14787  znunit  14807  psrval  14814  psrgrp  14840  psrneg  14842  mplval2g  14850  restuni2  15042  lmfval  15058  cnfval  15059  cnpfval  15060  txtopon  15127  txcnp  15136  upxp  15137  txrest  15141  cnmptcom  15163  bl2in  15268  xblss2  15270  isxms2  15317  setsmsdsg  15345  setsmstsetg  15346  metss  15359  resubmet  15421  expcn  15434  cncfcncntop  15458  dvidlemap  15556  dvidrelem  15557  dvidsslem  15558  dvcnp2cntop  15564  dvcoapbr  15572  dvcjbr  15573  dvexp  15576  dvexp2  15577  dvrecap  15578  plyaddlem1  15612  plymullem1  15613  plycolemc  15623  plycjlemc  15625  dvply1  15630  efimpi  15684  tangtx  15703  logdivlti  15746  cxpexprp  15760  rpcxpsub  15773  rpabscxpbnd  15805  rprelogbdiv  15822  binom4  15844  pellexlem2  15846  mpodvdsmulf1o  15858  0sgmppw  15861  lgslem1  15873  lgsmod  15899  lgsdilem  15900  lgsdi  15910  lgsne0  15911  lgsdirnn0  15920  lgsdinn0  15921  lgseisenlem2  15944  lgseisenlem3  15945  lgsquadlem2  15951  lgsquadlem3  15952  lgsquad2lem1  15954  lgsquad3  15957  2lgslem3  15974  2lgsoddprmlem2  15979  2sqlem4  15991  basvtxval2dom  16029  edgfiedgval2dom  16030  setsvtx  16046  ushgredgedgloop  16223  usgr1vr  16243  wlkres  16374  clwwlkccatlem  16395  trlsegvdegfi  16462  eupth2lem3lem2fi  16464  eupth2lem3lem6fi  16466  eupth2lem3lem4fi  16468  depindlem3  16503  bj-charfundcALT  16579  pw1ndom3lem  16763  pw1ndom3  16764  sssneq  16776  0nninf  16782  nnnninfex  16800  nninfnfiinf  16801  repiecele0  16810  trilpolemisumle  16822  qdiff  16833  gsumgfsum  16866  gfsump1  16868