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 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 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  3189  ifsbdc  3622  ifeq1dadc  3640  ifeq2dadc  3641  eqifdc  3646  ifnotdc  3648  2if2dc  3649  ifandc  3650  ifordc  3651  onsucuni2  4668  relop  4886  riinint  4999  iotauni  5306  fniinfv  5713  fsn2  5829  fmptapd  5853  fconst2g  5877  fniunfv  5913  ofres  6259  ofco  6263  caofid1  6273  caofid2  6274  fsuppeq  6425  fsuppeqg  6426  frecsuclem  6615  frecrdg  6617  oasuc  6675  nnacom  6695  nnaass  6696  nndi  6697  nnmass  6698  nnmsucr  6699  nnmcom  6700  funresdfunsndc  6717  uniqs2  6807  en1bg  7017  fundmen  7024  1dom1el  7036  1domsn  7044  pw2f1odclem  7063  mapxpen  7077  xpmapenlem  7078  phplem4dom  7091  en2eqpr  7142  sbthlemi5  7203  omp1eomlem  7336  difinfsnlem  7341  ctmlemr  7350  ctssdccl  7353  ctssdc  7355  infnninf  7366  infnninfOLD  7367  nnnninfeq  7370  pr2cv1  7443  exmidonfinlem  7447  exmidmotap  7523  addcmpblnq  7630  distrnqg  7650  ltexnqq  7671  addcmpblnq0  7706  nqnq0a  7717  nqnq0m  7718  nq0m0r  7719  nq0a0  7720  nnanq0  7721  distrnq0  7722  prarloclemlo  7757  prarloclemcalc  7765  genpassl  7787  genpassu  7788  ltsosr  8027  0idsr  8030  1idsr  8031  mulextsr1lem  8043  cnegex  8399  subsub3  8453  subadd4  8465  mulneg12  8618  mulsub  8622  apreap  8809  cru  8824  recextlem1  8873  cju  9183  ofnegsub  9184  halfaddsub  9420  nn0supp  9498  nneo  9627  zeo2  9630  uzin  9833  xaddcom  10140  xaddass  10148  xleaddadd  10166  iccf1o  10284  fzsuc2  10359  fldiv4lem1div2uz2  10612  flqeqceilz  10626  zmod1congr  10649  modqcyc  10667  modqcyc2  10668  modqaddabs  10670  modqmul1  10685  modqaddmulmod  10699  addmodlteq  10706  frec2uzrdg  10717  frecuzrdgsuctlem  10731  seq3val  10768  seqvalcd  10769  seq3fveq2  10783  seqfveq2g  10785  seq3split  10796  seqsplitg  10797  seqf1oglem2a  10826  seqf1oglem2  10828  seqfeq4g  10839  seq3distr  10840  ser0f  10842  expp1  10854  mulexp  10886  mulexpzap  10887  expadd  10889  expaddzap  10891  expmul  10892  expmulzap  10893  expsubap  10895  expdivap  10898  subsq  10954  mulbinom2  10964  binom3  10965  bernneq  10968  modqexp  10974  nn0opthd  11030  faclbnd  11049  faclbnd6  11052  bccmpl  11062  bcp1n  11069  zfz1isolemiso  11149  seq3coll  11152  hashtpglem  11156  ccatsymb  11228  ccatval1lsw  11230  ccatass  11234  eqs1  11254  lswccats1fst  11270  swrdsb0eq  11295  swrdsbslen  11296  swrds1  11298  ccatswrd  11300  pfxres  11311  ccatpfx  11331  pfxpfx  11338  cats1un  11351  swrdccatin1  11355  pfxccatin12  11363  swrdccat  11365  pfxccat3a  11368  swrdccat3b  11370  shftval2  11449  shftval4  11451  seq3shft  11461  crre  11480  remim  11483  remullem  11494  cjexp  11516  cnrecnv  11533  resqrexlemlo  11636  resqrexlemcalc1  11637  resqrexlemcalc2  11638  resqrexlemcalc3  11639  resqrexlemnm  11641  rsqrmo  11650  abscj  11675  absid  11694  absre  11700  recvalap  11720  maxabsle  11827  maxltsup  11841  2zsupmax  11849  minabs  11859  bdtrilem  11862  bdtri  11863  2zinfmin  11866  xrmaxiflemab  11870  xrmaxiflemcom  11872  xrmaxadd  11884  xrbdtri  11899  iooinsup  11900  climaddc1  11952  climmulc2  11954  climsubc1  11955  climsubc2  11956  climcvg1nlem  11972  summodclem3  12004  zsumdc  12008  isum  12009  isumz  12013  isumss  12015  fisumss  12016  fsum3cvg2  12018  fsumadd  12030  isummulc2  12050  sumsplitdc  12056  fsum2dlemstep  12058  fisumcom2  12062  fisum0diag2  12071  fsumconst  12078  telfsumo  12090  fsumparts  12094  fsumrelem  12095  binomlem  12107  isumshft  12114  isumsplit  12115  arisum  12122  arisum2  12123  trireciplem  12124  geolim2  12136  geo2sum  12138  0.999...  12145  cvgratz  12156  mertensabs  12161  clim2prod  12163  prodf1f  12167  prodmodclem2a  12200  zproddc  12203  iprodap  12204  iprodap0  12206  fprodseq  12207  prod1dc  12210  prodssdc  12213  fprod2dlemstep  12246  fprodcom2fi  12250  fproddivap  12254  ef0lem  12284  efval2  12289  ege2le3  12295  efaddlem  12298  efsub  12305  eftlub  12314  efsep  12315  tanval3ap  12338  efi4p  12341  sinneg  12350  sinmul  12368  sincossq  12372  cos2t  12374  demoivreALT  12398  eirraplem  12401  dvdsmodexp  12419  odd2np1  12497  omoe  12520  divalglemex  12546  divalglemeuneg  12547  divalgmod  12551  flodddiv4  12560  bitsp1  12575  bitsinv1lem  12585  bitsinv1  12586  gcdneg  12616  gcdaddm  12618  modgcd  12625  bezoutlemnewy  12630  gcdass  12649  gcdmultiple  12654  nninfctlemfo  12674  algrp1  12681  lcmneg  12709  lcmgcdeq  12718  lcmass  12720  cncongr2  12739  prmexpb  12786  sqrt2irr  12797  2sqpwodd  12811  qnumdenbi  12827  phiprmpw  12857  eulerthlema  12865  fermltl  12869  prmdiveq  12871  modprm0  12890  pythagtriplem1  12901  pythagtriplem12  12911  pythagtriplem14  12913  pythagtriplem15  12914  pythagtriplem16  12915  pythagtriplem17  12916  pythagtriplem19  12918  pcpremul  12929  pcneg  12961  pcgcd  12965  pc2dvds  12966  pcaddlem  12975  pcprod  12982  fldivp1  12984  pcbc  12987  prmpwdvds  12991  pockthlem  12992  mul4sqlem  13029  4sqlem11  13037  4sqlem12  13038  4sqlem17  13043  ctiunctlemfo  13123  ressval3d  13218  resseqnbasd  13219  prdsval  13419  imasival  13452  qusval  13469  plusfeqg  13510  sgrp1  13557  idmhm  13615  resmhm2  13634  mhmeql  13638  grppropstrg  13665  grpinvinv  13713  grp1  13752  imasgrp2  13760  mulgnngsum  13777  mulginvcom  13797  mulgnndir  13801  mulgdir  13804  mulgneg2  13806  mulgnnass  13807  mulgass  13809  mulgsubdir  13812  trivsubgd  13850  nmzsubg  13860  qussub  13887  idghm  13909  ablinvadd  13960  ablsub2inv  13961  eqgabl  13980  mgpplusgg  14001  mgpbasg  14003  mgpscag  14004  mgptsetg  14005  mgpdsg  14007  mgpress  14008  srgpcomp  14067  srgpcompp  14068  ringo2times  14105  ring1eq0  14125  ring1  14136  opprmulfvalg  14147  crngoppr  14149  opprsllem  14151  oppr1g  14159  opprunitd  14188  rdivmuldivd  14222  rhmunitinv  14256  scafeqg  14387  lmodvsubval2  14421  lmodsubdi  14423  rmodislmod  14430  sralemg  14517  sraipg  14523  crng2idl  14610  cnfldmulg  14655  cnfldexp  14656  cnfldui  14668  mulgrhm2  14689  zrhrhmb  14701  zlmvscag  14712  znval2  14717  znbaslemnn  14718  znunit  14738  psrval  14745  psrgrp  14769  psrneg  14771  mplval2g  14779  restuni2  14971  lmfval  14987  cnfval  14988  cnpfval  14989  txtopon  15056  txcnp  15065  upxp  15066  txrest  15070  cnmptcom  15092  bl2in  15197  xblss2  15199  isxms2  15246  setsmsdsg  15274  setsmstsetg  15275  metss  15288  resubmet  15350  expcn  15363  cncfcncntop  15387  dvidlemap  15485  dvidrelem  15486  dvidsslem  15487  dvcnp2cntop  15493  dvcoapbr  15501  dvcjbr  15502  dvexp  15505  dvexp2  15506  dvrecap  15507  plyaddlem1  15541  plymullem1  15542  plycolemc  15552  plycjlemc  15554  dvply1  15559  efimpi  15613  tangtx  15632  logdivlti  15675  cxpexprp  15689  rpcxpsub  15702  rpabscxpbnd  15734  rprelogbdiv  15751  binom4  15773  pellexlem2  15775  mpodvdsmulf1o  15787  0sgmppw  15790  lgslem1  15802  lgsmod  15828  lgsdilem  15829  lgsdi  15839  lgsne0  15840  lgsdirnn0  15849  lgsdinn0  15850  lgseisenlem2  15873  lgseisenlem3  15874  lgsquadlem2  15880  lgsquadlem3  15881  lgsquad2lem1  15883  lgsquad3  15886  2lgslem3  15903  2lgsoddprmlem2  15908  2sqlem4  15920  basvtxval2dom  15958  edgfiedgval2dom  15959  setsvtx  15975  ushgredgedgloop  16152  usgr1vr  16172  wlkres  16303  clwwlkccatlem  16324  trlsegvdegfi  16391  eupth2lem3lem2fi  16393  eupth2lem3lem6fi  16395  eupth2lem3lem4fi  16397  depindlem3  16432  bj-charfundcALT  16508  pw1ndom3lem  16692  pw1ndom3  16693  2omap  16698  sssneq  16707  0nninf  16713  nnnninfex  16731  nninfnfiinf  16732  repiecele0  16741  trilpolemisumle  16753  qdiff  16764  gsumgfsum  16796  gfsump1  16798