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  3186  ifsbdc  3616  ifeq1dadc  3634  ifeq2dadc  3635  eqifdc  3640  ifnotdc  3642  2if2dc  3643  ifandc  3644  ifordc  3645  onsucuni2  4660  relop  4878  riinint  4991  iotauni  5297  fniinfv  5700  fsn2  5817  fmptapd  5840  fconst2g  5864  fniunfv  5898  ofres  6245  ofco  6249  caofid1  6259  caofid2  6260  frecsuclem  6567  frecrdg  6569  oasuc  6627  nnacom  6647  nnaass  6648  nndi  6649  nnmass  6650  nnmsucr  6651  nnmcom  6652  funresdfunsndc  6669  uniqs2  6759  en1bg  6969  fundmen  6976  1dom1el  6988  1domsn  6996  pw2f1odclem  7015  mapxpen  7029  xpmapenlem  7030  phplem4dom  7043  en2eqpr  7092  sbthlemi5  7151  omp1eomlem  7284  difinfsnlem  7289  ctmlemr  7298  ctssdccl  7301  ctssdc  7303  infnninf  7314  infnninfOLD  7315  nnnninfeq  7318  pr2cv1  7391  exmidonfinlem  7394  exmidmotap  7470  addcmpblnq  7577  distrnqg  7597  ltexnqq  7618  addcmpblnq0  7653  nqnq0a  7664  nqnq0m  7665  nq0m0r  7666  nq0a0  7667  nnanq0  7668  distrnq0  7669  prarloclemlo  7704  prarloclemcalc  7712  genpassl  7734  genpassu  7735  ltsosr  7974  0idsr  7977  1idsr  7978  mulextsr1lem  7990  cnegex  8347  subsub3  8401  subadd4  8413  mulneg12  8566  mulsub  8570  apreap  8757  cru  8772  recextlem1  8821  cju  9131  ofnegsub  9132  halfaddsub  9368  nn0supp  9444  nneo  9573  zeo2  9576  uzin  9779  xaddcom  10086  xaddass  10094  xleaddadd  10112  iccf1o  10229  fzsuc2  10304  fldiv4lem1div2uz2  10556  flqeqceilz  10570  zmod1congr  10593  modqcyc  10611  modqcyc2  10612  modqaddabs  10614  modqmul1  10629  modqaddmulmod  10643  addmodlteq  10650  frec2uzrdg  10661  frecuzrdgsuctlem  10675  seq3val  10712  seqvalcd  10713  seq3fveq2  10727  seqfveq2g  10729  seq3split  10740  seqsplitg  10741  seqf1oglem2a  10770  seqf1oglem2  10772  seqfeq4g  10783  seq3distr  10784  ser0f  10786  expp1  10798  mulexp  10830  mulexpzap  10831  expadd  10833  expaddzap  10835  expmul  10836  expmulzap  10837  expsubap  10839  expdivap  10842  subsq  10898  mulbinom2  10908  binom3  10909  bernneq  10912  modqexp  10918  nn0opthd  10974  faclbnd  10993  faclbnd6  10996  bccmpl  11006  bcp1n  11013  zfz1isolemiso  11093  seq3coll  11096  ccatsymb  11169  ccatval1lsw  11171  ccatass  11175  eqs1  11195  lswccats1fst  11211  swrdsb0eq  11236  swrdsbslen  11237  swrds1  11239  ccatswrd  11241  pfxres  11252  ccatpfx  11272  pfxpfx  11279  cats1un  11292  swrdccatin1  11296  pfxccatin12  11304  swrdccat  11306  pfxccat3a  11309  swrdccat3b  11311  shftval2  11377  shftval4  11379  seq3shft  11389  crre  11408  remim  11411  remullem  11422  cjexp  11444  cnrecnv  11461  resqrexlemlo  11564  resqrexlemcalc1  11565  resqrexlemcalc2  11566  resqrexlemcalc3  11567  resqrexlemnm  11569  rsqrmo  11578  abscj  11603  absid  11622  absre  11628  recvalap  11648  maxabsle  11755  maxltsup  11769  2zsupmax  11777  minabs  11787  bdtrilem  11790  bdtri  11791  2zinfmin  11794  xrmaxiflemab  11798  xrmaxiflemcom  11800  xrmaxadd  11812  xrbdtri  11827  iooinsup  11828  climaddc1  11880  climmulc2  11882  climsubc1  11883  climsubc2  11884  climcvg1nlem  11900  summodclem3  11931  zsumdc  11935  isum  11936  isumz  11940  isumss  11942  fisumss  11943  fsum3cvg2  11945  fsumadd  11957  isummulc2  11977  sumsplitdc  11983  fsum2dlemstep  11985  fisumcom2  11989  fisum0diag2  11998  fsumconst  12005  telfsumo  12017  fsumparts  12021  fsumrelem  12022  binomlem  12034  isumshft  12041  isumsplit  12042  arisum  12049  arisum2  12050  trireciplem  12051  geolim2  12063  geo2sum  12065  0.999...  12072  cvgratz  12083  mertensabs  12088  clim2prod  12090  prodf1f  12094  prodmodclem2a  12127  zproddc  12130  iprodap  12131  iprodap0  12133  fprodseq  12134  prod1dc  12137  prodssdc  12140  fprod2dlemstep  12173  fprodcom2fi  12177  fproddivap  12181  ef0lem  12211  efval2  12216  ege2le3  12222  efaddlem  12225  efsub  12232  eftlub  12241  efsep  12242  tanval3ap  12265  efi4p  12268  sinneg  12277  sinmul  12295  sincossq  12299  cos2t  12301  demoivreALT  12325  eirraplem  12328  dvdsmodexp  12346  odd2np1  12424  omoe  12447  divalglemex  12473  divalglemeuneg  12474  divalgmod  12478  flodddiv4  12487  bitsp1  12502  bitsinv1lem  12512  bitsinv1  12513  gcdneg  12543  gcdaddm  12545  modgcd  12552  bezoutlemnewy  12557  gcdass  12576  gcdmultiple  12581  nninfctlemfo  12601  algrp1  12608  lcmneg  12636  lcmgcdeq  12645  lcmass  12647  cncongr2  12666  prmexpb  12713  sqrt2irr  12724  2sqpwodd  12738  qnumdenbi  12754  phiprmpw  12784  eulerthlema  12792  fermltl  12796  prmdiveq  12798  modprm0  12817  pythagtriplem1  12828  pythagtriplem12  12838  pythagtriplem14  12840  pythagtriplem15  12841  pythagtriplem16  12842  pythagtriplem17  12843  pythagtriplem19  12845  pcpremul  12856  pcneg  12888  pcgcd  12892  pc2dvds  12893  pcaddlem  12902  pcprod  12909  fldivp1  12911  pcbc  12914  prmpwdvds  12918  pockthlem  12919  mul4sqlem  12956  4sqlem11  12964  4sqlem12  12965  4sqlem17  12970  ctiunctlemfo  13050  ressval3d  13145  resseqnbasd  13146  prdsval  13346  imasival  13379  qusval  13396  plusfeqg  13437  sgrp1  13484  idmhm  13542  resmhm2  13561  mhmeql  13565  grppropstrg  13592  grpinvinv  13640  grp1  13679  imasgrp2  13687  mulgnngsum  13704  mulginvcom  13724  mulgnndir  13728  mulgdir  13731  mulgneg2  13733  mulgnnass  13734  mulgass  13736  mulgsubdir  13739  trivsubgd  13777  nmzsubg  13787  qussub  13814  idghm  13836  ablinvadd  13887  ablsub2inv  13888  eqgabl  13907  mgpplusgg  13927  mgpbasg  13929  mgpscag  13930  mgptsetg  13931  mgpdsg  13933  mgpress  13934  srgpcomp  13993  srgpcompp  13994  ringo2times  14031  ring1eq0  14051  ring1  14062  opprmulfvalg  14073  crngoppr  14075  opprsllem  14077  oppr1g  14085  opprunitd  14114  rdivmuldivd  14148  rhmunitinv  14182  scafeqg  14312  lmodvsubval2  14346  lmodsubdi  14348  rmodislmod  14355  sralemg  14442  sraipg  14448  crng2idl  14535  cnfldmulg  14580  cnfldexp  14581  cnfldui  14593  mulgrhm2  14614  zrhrhmb  14626  zlmvscag  14637  znval2  14642  znbaslemnn  14643  znunit  14663  psrval  14670  psrgrp  14689  psrneg  14691  mplval2g  14699  restuni2  14891  lmfval  14907  cnfval  14908  cnpfval  14909  txtopon  14976  txcnp  14985  upxp  14986  txrest  14990  cnmptcom  15012  bl2in  15117  xblss2  15119  isxms2  15166  setsmsdsg  15194  setsmstsetg  15195  metss  15208  resubmet  15270  expcn  15283  cncfcncntop  15307  dvidlemap  15405  dvidrelem  15406  dvidsslem  15407  dvcnp2cntop  15413  dvcoapbr  15421  dvcjbr  15422  dvexp  15425  dvexp2  15426  dvrecap  15427  plyaddlem1  15461  plymullem1  15462  plycolemc  15472  plycjlemc  15474  dvply1  15479  efimpi  15533  tangtx  15552  logdivlti  15595  cxpexprp  15609  rpcxpsub  15622  rpabscxpbnd  15654  rprelogbdiv  15671  binom4  15693  mpodvdsmulf1o  15704  0sgmppw  15707  lgslem1  15719  lgsmod  15745  lgsdilem  15746  lgsdi  15756  lgsne0  15757  lgsdirnn0  15766  lgsdinn0  15767  lgseisenlem2  15790  lgseisenlem3  15791  lgsquadlem2  15797  lgsquadlem3  15798  lgsquad2lem1  15800  lgsquad3  15803  2lgslem3  15820  2lgsoddprmlem2  15825  2sqlem4  15837  basvtxval2dom  15875  edgfiedgval2dom  15876  setsvtx  15892  ushgredgedgloop  16067  usgr1vr  16087  wlkres  16174  clwwlkccatlem  16195  bj-charfundcALT  16340  pw1ndom3lem  16524  pw1ndom3  16525  2omap  16530  sssneq  16539  0nninf  16542  nnnninfex  16560  nninfnfiinf  16561  trilpolemisumle  16578