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  4655  relop  4871  riinint  4984  iotauni  5290  fniinfv  5691  fsn2  5808  fmptapd  5829  fconst2g  5853  fniunfv  5885  ofres  6231  ofco  6235  caofid1  6245  caofid2  6246  frecsuclem  6550  frecrdg  6552  oasuc  6608  nnacom  6628  nnaass  6629  nndi  6630  nnmass  6631  nnmsucr  6632  nnmcom  6633  funresdfunsndc  6650  uniqs2  6740  en1bg  6950  fundmen  6957  1domsn  6974  pw2f1odclem  6991  mapxpen  7005  xpmapenlem  7006  phplem4dom  7019  en2eqpr  7065  sbthlemi5  7124  omp1eomlem  7257  difinfsnlem  7262  ctmlemr  7271  ctssdccl  7274  ctssdc  7276  infnninf  7287  infnninfOLD  7288  nnnninfeq  7291  pr2cv1  7364  exmidonfinlem  7367  exmidmotap  7443  addcmpblnq  7550  distrnqg  7570  ltexnqq  7591  addcmpblnq0  7626  nqnq0a  7637  nqnq0m  7638  nq0m0r  7639  nq0a0  7640  nnanq0  7641  distrnq0  7642  prarloclemlo  7677  prarloclemcalc  7685  genpassl  7707  genpassu  7708  ltsosr  7947  0idsr  7950  1idsr  7951  mulextsr1lem  7963  cnegex  8320  subsub3  8374  subadd4  8386  mulneg12  8539  mulsub  8543  apreap  8730  cru  8745  recextlem1  8794  cju  9104  ofnegsub  9105  halfaddsub  9341  nn0supp  9417  nneo  9546  zeo2  9549  uzin  9751  xaddcom  10053  xaddass  10061  xleaddadd  10079  iccf1o  10196  fzsuc2  10271  fldiv4lem1div2uz2  10521  flqeqceilz  10535  zmod1congr  10558  modqcyc  10576  modqcyc2  10577  modqaddabs  10579  modqmul1  10594  modqaddmulmod  10608  addmodlteq  10615  frec2uzrdg  10626  frecuzrdgsuctlem  10640  seq3val  10677  seqvalcd  10678  seq3fveq2  10692  seqfveq2g  10694  seq3split  10705  seqsplitg  10706  seqf1oglem2a  10735  seqf1oglem2  10737  seqfeq4g  10748  seq3distr  10749  ser0f  10751  expp1  10763  mulexp  10795  mulexpzap  10796  expadd  10798  expaddzap  10800  expmul  10801  expmulzap  10802  expsubap  10804  expdivap  10807  subsq  10863  mulbinom2  10873  binom3  10874  bernneq  10877  modqexp  10883  nn0opthd  10939  faclbnd  10958  faclbnd6  10961  bccmpl  10971  bcp1n  10978  zfz1isolemiso  11056  seq3coll  11059  ccatsymb  11132  ccatval1lsw  11134  ccatass  11138  eqs1  11156  lswccats1fst  11170  swrdsb0eq  11192  swrdsbslen  11193  swrds1  11195  ccatswrd  11197  pfxres  11208  ccatpfx  11228  pfxpfx  11235  cats1un  11248  swrdccatin1  11252  pfxccatin12  11260  swrdccat  11262  pfxccat3a  11265  swrdccat3b  11267  shftval2  11332  shftval4  11334  seq3shft  11344  crre  11363  remim  11366  remullem  11377  cjexp  11399  cnrecnv  11416  resqrexlemlo  11519  resqrexlemcalc1  11520  resqrexlemcalc2  11521  resqrexlemcalc3  11522  resqrexlemnm  11524  rsqrmo  11533  abscj  11558  absid  11577  absre  11583  recvalap  11603  maxabsle  11710  maxltsup  11724  2zsupmax  11732  minabs  11742  bdtrilem  11745  bdtri  11746  2zinfmin  11749  xrmaxiflemab  11753  xrmaxiflemcom  11755  xrmaxadd  11767  xrbdtri  11782  iooinsup  11783  climaddc1  11835  climmulc2  11837  climsubc1  11838  climsubc2  11839  climcvg1nlem  11855  summodclem3  11886  zsumdc  11890  isum  11891  isumz  11895  isumss  11897  fisumss  11898  fsum3cvg2  11900  fsumadd  11912  isummulc2  11932  sumsplitdc  11938  fsum2dlemstep  11940  fisumcom2  11944  fisum0diag2  11953  fsumconst  11960  telfsumo  11972  fsumparts  11976  fsumrelem  11977  binomlem  11989  isumshft  11996  isumsplit  11997  arisum  12004  arisum2  12005  trireciplem  12006  geolim2  12018  geo2sum  12020  0.999...  12027  cvgratz  12038  mertensabs  12043  clim2prod  12045  prodf1f  12049  prodmodclem2a  12082  zproddc  12085  iprodap  12086  iprodap0  12088  fprodseq  12089  prod1dc  12092  prodssdc  12095  fprod2dlemstep  12128  fprodcom2fi  12132  fproddivap  12136  ef0lem  12166  efval2  12171  ege2le3  12177  efaddlem  12180  efsub  12187  eftlub  12196  efsep  12197  tanval3ap  12220  efi4p  12223  sinneg  12232  sinmul  12250  sincossq  12254  cos2t  12256  demoivreALT  12280  eirraplem  12283  dvdsmodexp  12301  odd2np1  12379  omoe  12402  divalglemex  12428  divalglemeuneg  12429  divalgmod  12433  flodddiv4  12442  bitsp1  12457  bitsinv1lem  12467  bitsinv1  12468  gcdneg  12498  gcdaddm  12500  modgcd  12507  bezoutlemnewy  12512  gcdass  12531  gcdmultiple  12536  nninfctlemfo  12556  algrp1  12563  lcmneg  12591  lcmgcdeq  12600  lcmass  12602  cncongr2  12621  prmexpb  12668  sqrt2irr  12679  2sqpwodd  12693  qnumdenbi  12709  phiprmpw  12739  eulerthlema  12747  fermltl  12751  prmdiveq  12753  modprm0  12772  pythagtriplem1  12783  pythagtriplem12  12793  pythagtriplem14  12795  pythagtriplem15  12796  pythagtriplem16  12797  pythagtriplem17  12798  pythagtriplem19  12800  pcpremul  12811  pcneg  12843  pcgcd  12847  pc2dvds  12848  pcaddlem  12857  pcprod  12864  fldivp1  12866  pcbc  12869  prmpwdvds  12873  pockthlem  12874  mul4sqlem  12911  4sqlem11  12919  4sqlem12  12920  4sqlem17  12925  ctiunctlemfo  13005  ressval3d  13100  resseqnbasd  13101  prdsval  13301  imasival  13334  qusval  13351  plusfeqg  13392  sgrp1  13439  idmhm  13497  resmhm2  13516  mhmeql  13520  grppropstrg  13547  grpinvinv  13595  grp1  13634  imasgrp2  13642  mulgnngsum  13659  mulginvcom  13679  mulgnndir  13683  mulgdir  13686  mulgneg2  13688  mulgnnass  13689  mulgass  13691  mulgsubdir  13694  trivsubgd  13732  nmzsubg  13742  qussub  13769  idghm  13791  ablinvadd  13842  ablsub2inv  13843  eqgabl  13862  mgpplusgg  13882  mgpbasg  13884  mgpscag  13885  mgptsetg  13886  mgpdsg  13888  mgpress  13889  srgpcomp  13948  srgpcompp  13949  ringo2times  13986  ring1eq0  14006  ring1  14017  opprmulfvalg  14028  crngoppr  14030  opprsllem  14032  oppr1g  14040  opprunitd  14068  rdivmuldivd  14102  rhmunitinv  14136  scafeqg  14266  lmodvsubval2  14300  lmodsubdi  14302  rmodislmod  14309  sralemg  14396  sraipg  14402  crng2idl  14489  cnfldmulg  14534  cnfldexp  14535  cnfldui  14547  mulgrhm2  14568  zrhrhmb  14580  zlmvscag  14591  znval2  14596  znbaslemnn  14597  znunit  14617  psrval  14624  psrgrp  14643  psrneg  14645  mplval2g  14653  restuni2  14845  lmfval  14860  cnfval  14862  cnpfval  14863  txtopon  14930  txcnp  14939  upxp  14940  txrest  14944  cnmptcom  14966  bl2in  15071  xblss2  15073  isxms2  15120  setsmsdsg  15148  setsmstsetg  15149  metss  15162  resubmet  15224  expcn  15237  cncfcncntop  15261  dvidlemap  15359  dvidrelem  15360  dvidsslem  15361  dvcnp2cntop  15367  dvcoapbr  15375  dvcjbr  15376  dvexp  15379  dvexp2  15380  dvrecap  15381  plyaddlem1  15415  plymullem1  15416  plycolemc  15426  plycjlemc  15428  dvply1  15433  efimpi  15487  tangtx  15506  logdivlti  15549  cxpexprp  15563  rpcxpsub  15576  rpabscxpbnd  15608  rprelogbdiv  15625  binom4  15647  mpodvdsmulf1o  15658  0sgmppw  15661  lgslem1  15673  lgsmod  15699  lgsdilem  15700  lgsdi  15710  lgsne0  15711  lgsdirnn0  15720  lgsdinn0  15721  lgseisenlem2  15744  lgseisenlem3  15745  lgsquadlem2  15751  lgsquadlem3  15752  lgsquad2lem1  15754  lgsquad3  15757  2lgslem3  15774  2lgsoddprmlem2  15779  2sqlem4  15791  basvtxval2dom  15829  edgfiedgval2dom  15830  setsvtx  15846  ushgredgedgloop  16020  bj-charfundcALT  16130  1dom1el  16312  2omap  16318  sssneq  16327  0nninf  16329  nnnninfex  16347  nninfnfiinf  16348  trilpolemisumle  16365