Theorem eqtr4d 2229

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 2199	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 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:  3eqtr2d  2232  3eqtr2rd  2233  3eqtr4d  2236  3eqtr4rd  2237  3eqtr4a  2252  sbnfc2  3142  ifsbdc  3570  ifeq1dadc  3588  ifeq2dadc  3589  eqifdc  3593  ifnotdc  3595  ifandc  3596  ifordc  3597  onsucuni2  4597  relop  4813  riinint  4924  iotauni  5228  fniinfv  5616  fsn2  5733  fmptapd  5750  fconst2g  5774  fniunfv  5806  ofres  6147  ofco  6151  frecsuclem  6461  frecrdg  6463  oasuc  6519  nnacom  6539  nnaass  6540  nndi  6541  nnmass  6542  nnmsucr  6543  nnmcom  6544  funresdfunsndc  6561  uniqs2  6651  en1bg  6856  fundmen  6862  1domsn  6875  pw2f1odclem  6892  mapxpen  6906  xpmapenlem  6907  phplem4dom  6920  en2eqpr  6965  sbthlemi5  7022  omp1eomlem  7155  difinfsnlem  7160  ctmlemr  7169  ctssdccl  7172  ctssdc  7174  infnninf  7185  infnninfOLD  7186  nnnninfeq  7189  exmidonfinlem  7255  exmidmotap  7323  addcmpblnq  7429  distrnqg  7449  ltexnqq  7470  addcmpblnq0  7505  nqnq0a  7516  nqnq0m  7517  nq0m0r  7518  nq0a0  7519  nnanq0  7520  distrnq0  7521  prarloclemlo  7556  prarloclemcalc  7564  genpassl  7586  genpassu  7587  ltsosr  7826  0idsr  7829  1idsr  7830  mulextsr1lem  7842  cnegex  8199  subsub3  8253  subadd4  8265  mulneg12  8418  mulsub  8422  apreap  8608  cru  8623  recextlem1  8672  cju  8982  ofnegsub  8983  halfaddsub  9219  nn0supp  9295  nneo  9423  zeo2  9426  uzin  9628  xaddcom  9930  xaddass  9938  xleaddadd  9956  iccf1o  10073  fzsuc2  10148  fldiv4lem1div2uz2  10378  flqeqceilz  10392  zmod1congr  10415  modqcyc  10433  modqcyc2  10434  modqaddabs  10436  modqmul1  10451  modqaddmulmod  10465  addmodlteq  10472  frec2uzrdg  10483  frecuzrdgsuctlem  10497  seq3val  10534  seqvalcd  10535  seq3fveq2  10549  seqfveq2g  10551  seq3split  10562  seqsplitg  10563  seqf1oglem2a  10592  seqf1oglem2  10594  seqfeq4g  10605  seq3distr  10606  ser0f  10608  expp1  10620  mulexp  10652  mulexpzap  10653  expadd  10655  expaddzap  10657  expmul  10658  expmulzap  10659  expsubap  10661  expdivap  10664  subsq  10720  mulbinom2  10730  binom3  10731  bernneq  10734  modqexp  10740  nn0opthd  10796  faclbnd  10815  faclbnd6  10818  bccmpl  10828  bcp1n  10835  zfz1isolemiso  10913  seq3coll  10916  shftval2  10973  shftval4  10975  seq3shft  10985  crre  11004  remim  11007  remullem  11018  cjexp  11040  cnrecnv  11057  resqrexlemlo  11160  resqrexlemcalc1  11161  resqrexlemcalc2  11162  resqrexlemcalc3  11163  resqrexlemnm  11165  rsqrmo  11174  abscj  11199  absid  11218  absre  11224  recvalap  11244  maxabsle  11351  maxltsup  11365  2zsupmax  11372  minabs  11382  bdtrilem  11385  bdtri  11386  2zinfmin  11389  xrmaxiflemab  11393  xrmaxiflemcom  11395  xrmaxadd  11407  xrbdtri  11422  iooinsup  11423  climaddc1  11475  climmulc2  11477  climsubc1  11478  climsubc2  11479  climcvg1nlem  11495  summodclem3  11526  zsumdc  11530  isum  11531  isumz  11535  isumss  11537  fisumss  11538  fsum3cvg2  11540  fsumadd  11552  isummulc2  11572  sumsplitdc  11578  fsum2dlemstep  11580  fisumcom2  11584  fisum0diag2  11593  fsumconst  11600  telfsumo  11612  fsumparts  11616  fsumrelem  11617  binomlem  11629  isumshft  11636  isumsplit  11637  arisum  11644  arisum2  11645  trireciplem  11646  geolim2  11658  geo2sum  11660  0.999...  11667  cvgratz  11678  mertensabs  11683  clim2prod  11685  prodf1f  11689  prodmodclem2a  11722  zproddc  11725  iprodap  11726  iprodap0  11728  fprodseq  11729  prod1dc  11732  prodssdc  11735  fprod2dlemstep  11768  fprodcom2fi  11772  fproddivap  11776  ef0lem  11806  efval2  11811  ege2le3  11817  efaddlem  11820  efsub  11827  eftlub  11836  efsep  11837  tanval3ap  11860  efi4p  11863  sinneg  11872  sinmul  11890  sincossq  11894  cos2t  11896  demoivreALT  11920  eirraplem  11923  dvdsmodexp  11941  odd2np1  12017  omoe  12040  divalglemex  12066  divalglemeuneg  12067  divalgmod  12071  flodddiv4  12078  gcdneg  12122  gcdaddm  12124  modgcd  12131  bezoutlemnewy  12136  gcdass  12155  gcdmultiple  12160  nninfctlemfo  12180  algrp1  12187  lcmneg  12215  lcmgcdeq  12224  lcmass  12226  cncongr2  12245  prmexpb  12292  sqrt2irr  12303  2sqpwodd  12317  qnumdenbi  12333  phiprmpw  12363  eulerthlema  12371  fermltl  12375  prmdiveq  12377  modprm0  12395  pythagtriplem1  12406  pythagtriplem12  12416  pythagtriplem14  12418  pythagtriplem15  12419  pythagtriplem16  12420  pythagtriplem17  12421  pythagtriplem19  12423  pcpremul  12434  pcneg  12466  pcgcd  12470  pc2dvds  12471  pcaddlem  12480  pcprod  12487  fldivp1  12489  pcbc  12492  prmpwdvds  12496  pockthlem  12497  mul4sqlem  12534  4sqlem11  12542  4sqlem12  12543  4sqlem17  12548  ctiunctlemfo  12599  strslfv3  12667  ressval3d  12693  resseqnbasd  12694  imasival  12892  qusval  12909  plusfeqg  12950  sgrp1  12997  idmhm  13044  resmhm2  13063  mhmeql  13067  grppropstrg  13094  grpinvinv  13142  grp1  13181  imasgrp2  13183  mulgnngsum  13200  mulginvcom  13220  mulgnndir  13224  mulgdir  13227  mulgneg2  13229  mulgnnass  13230  mulgass  13232  mulgsubdir  13235  trivsubgd  13273  nmzsubg  13283  qussub  13310  idghm  13332  ablinvadd  13383  ablsub2inv  13384  eqgabl  13403  mgpplusgg  13423  mgpbasg  13425  mgpscag  13426  mgptsetg  13427  mgpdsg  13429  mgpress  13430  srgpcomp  13489  srgpcompp  13490  ringo2times  13527  ring1eq0  13547  ring1  13558  opprmulfvalg  13569  crngoppr  13571  opprsllem  13573  oppr1g  13581  opprunitd  13609  rdivmuldivd  13643  rhmunitinv  13677  scafeqg  13807  lmodvsubval2  13841  lmodsubdi  13843  rmodislmod  13850  sralemg  13937  sraipg  13943  crng2idl  14030  cnfldmulg  14075  cnfldexp  14076  cnfldui  14088  mulgrhm2  14109  zrhrhmb  14121  zlmvscag  14132  znval2  14137  znbaslemnn  14138  znunit  14158  psrval  14163  restuni2  14356  lmfval  14371  cnfval  14373  cnpfval  14374  txtopon  14441  txcnp  14450  upxp  14451  txrest  14455  cnmptcom  14477  bl2in  14582  xblss2  14584  isxms2  14631  setsmsdsg  14659  setsmstsetg  14660  metss  14673  resubmet  14735  expcn  14748  cncfcncntop  14772  dvidlemap  14870  dvidrelem  14871  dvidsslem  14872  dvcnp2cntop  14878  dvcoapbr  14886  dvcjbr  14887  dvexp  14890  dvexp2  14891  dvrecap  14892  plyaddlem1  14926  plymullem1  14927  plycolemc  14936  plycjlemc  14938  dvply1  14943  efimpi  14995  tangtx  15014  logdivlti  15057  cxpexprp  15071  rpcxpsub  15084  rpabscxpbnd  15114  rprelogbdiv  15130  binom4  15152  lgslem1  15157  lgsmod  15183  lgsdilem  15184  lgsdi  15194  lgsne0  15195  lgsdirnn0  15204  lgsdinn0  15205  lgseisenlem2  15228  lgseisenlem3  15229  lgsquadlem2  15235  lgsquadlem3  15236  lgsquad2lem1  15238  lgsquad3  15241  2lgslem3  15258  2lgsoddprmlem2  15263  2sqlem4  15275  bj-charfundcALT  15371  1dom1el  15553  sssneq  15562  0nninf  15564  trilpolemisumle  15598