Theorem eqtr4d 2274

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  3eqtr2d  2277  3eqtr2rd  2278  3eqtr4d  2281  3eqtr4rd  2282  3eqtr4a  2297  sbnfc2  3208  ifsbdc  3653  ifeq1dadc  3671  ifeq2dadc  3672  eqifdc  3677  ifnotdc  3679  2if2dc  3680  ifandc  3681  ifordc  3682  ifeqeqxdc  3687  onsucuni2  4713  relop  4932  riinint  5045  iotauni  5353  fniinfv  5764  fsn2  5885  fmptapd  5909  fconst2g  5933  fniunfv  5971  ofres  6321  ofco  6325  caofid1  6335  caofid2  6336  fsuppeq  6491  fsuppeqg  6492  frecsuclem  6682  frecrdg  6684  oasuc  6742  nnacom  6762  nnaass  6763  nndi  6764  nnmass  6765  nnmsucr  6766  nnmcom  6767  funresdfunsndc  6784  uniqs2  6874  en1bg  7093  fundmen  7100  1dom1el  7113  1domsn  7121  pw2f1odclem  7140  mapxpen  7154  xpmapenlem  7155  mapunen  7157  phplem4dom  7169  en2eqpr  7220  sbthlemi5  7285  2omap  7324  omp1eomlem  7440  difinfsnlem  7445  ctmlemr  7454  ctssdccl  7457  ctssdc  7459  infnninf  7470  infnninfOLD  7471  nnnninfeq  7474  pr2cv1  7547  exmidonfinlem  7551  exmidmotap  7633  addcmpblnq  7740  distrnqg  7760  ltexnqq  7781  addcmpblnq0  7816  nqnq0a  7827  nqnq0m  7828  nq0m0r  7829  nq0a0  7830  nnanq0  7831  distrnq0  7832  prarloclemlo  7867  prarloclemcalc  7875  genpassl  7897  genpassu  7898  ltsosr  8137  0idsr  8140  1idsr  8141  mulextsr1lem  8153  cnegex  8511  subsub3  8565  subadd4  8577  mulneg12  8731  mulsub  8735  apreap  8923  cru  8938  recextlem1  8987  cju  9299  ofnegsub  9301  halfaddsub  9550  nn0supp  9628  nneo  9759  zeo2  9762  uzin  9970  xaddcom  10279  xaddass  10287  xleaddadd  10305  iccf1o  10423  fzsuc2  10502  fldiv4lem1div2uz2  10761  flqeqceilz  10775  zmod1congr  10798  modqcyc  10816  modqcyc2  10817  modqaddabs  10819  modqmul1  10834  modqaddmulmod  10848  addmodlteq  10855  frec2uzrdg  10866  frecuzrdgsuctlem  10880  seq3val  10917  seqvalcd  10918  seq3fveq2  10932  seqfveq2g  10934  seq3split  10945  seqsplitg  10946  seqf1oglem2a  10975  seqf1oglem2  10977  seqfeq4g  10988  seq3distr  10989  ser0f  10991  expp1  11003  mulexp  11035  mulexpzap  11036  expadd  11038  expaddzap  11040  expmul  11041  expmulzap  11042  expsubap  11044  expdivap  11047  subsq  11103  mulbinom2  11113  binom3  11114  bernneq  11118  modqexp  11124  nn0opthd  11181  faclbnd  11200  faclbnd6  11203  bccmpl  11213  bcp1n  11220  hashfibclem  11303  hashfibc  11304  hashf1lem1  11306  hashf1  11308  zfz1isolemiso  11312  seq3coll  11315  hashtpglem  11319  ccatsymb  11391  ccatval1lsw  11393  ccatass  11397  eqs1  11417  lswccats1fst  11433  swrdsb0eq  11458  swrdsbslen  11459  swrds1  11461  ccatswrd  11463  pfxres  11474  ccatpfx  11494  pfxpfx  11501  cats1un  11514  swrdccatin1  11518  pfxccatin12  11526  swrdccat  11528  pfxccat3a  11531  swrdccat3b  11533  shftval2  11612  shftval4  11614  seq3shft  11624  crre  11643  remim  11646  remullem  11657  cjexp  11679  sq01  11681  cnrecnv  11697  resqrexlemlo  11800  resqrexlemcalc1  11801  resqrexlemcalc2  11802  resqrexlemcalc3  11803  resqrexlemnm  11805  rsqrmo  11814  abscj  11839  absid  11858  absre  11865  recvalap  11885  maxabsle  11992  maxltsup  12006  2zsupmax  12014  minabs  12025  bdtrilem  12029  bdtri  12030  2zinfmin  12033  xrmaxiflemab  12037  xrmaxiflemcom  12039  xrmaxadd  12051  xrbdtri  12066  iooinsup  12067  climaddc1  12119  climmulc2  12121  climsubc1  12122  climsubc2  12123  climcvg1nlem  12139  summodclem3  12171  zsumdc  12175  isum  12176  isumz  12180  isumss  12182  fisumss  12183  fsum3cvg2  12185  fsumadd  12197  isummulc2  12217  sumsplitdc  12223  fsum2dlemstep  12225  fisumcom2  12229  fisum0diag2  12238  fsumconst  12245  telfsumo  12257  fsumparts  12261  fsumrelem  12262  binomlem  12274  isumshft  12281  isumsplit  12282  arisum  12289  arisum2  12290  trireciplem  12291  geolim2  12303  geo2sum  12305  0.999...  12312  cvgratz  12323  mertensabs  12328  clim2prod  12330  prodf1f  12334  prodmodclem2a  12367  zproddc  12370  iprodap  12371  iprodap0  12373  fprodseq  12374  prod1dc  12377  prodssdc  12380  fprod2dlemstep  12413  fprodcom2fi  12417  fproddivap  12421  ef0lem  12451  efval2  12456  ege2le3  12462  efaddlem  12465  efsub  12472  eftlub  12481  efsep  12482  tanval3ap  12505  efi4p  12508  sinneg  12517  sinmul  12535  sincossq  12539  cos2t  12541  demoivreALT  12565  eirraplem  12568  dvdsmodexp  12586  odd2np1  12664  omoe  12687  divalglemex  12713  divalglemeuneg  12714  divalgmod  12718  flodddiv4  12727  bitsp1  12742  bitsinv1lem  12752  bitsinv1  12753  gcdneg  12783  gcdaddm  12785  modgcd  12792  bezoutlemnewy  12797  gcdass  12816  gcdmultiple  12821  nninfctlemfo  12841  algrp1  12848  lcmneg  12876  lcmgcdeq  12885  lcmass  12887  cncongr2  12906  prmexpb  12954  sqrt2irr  12965  2sqpwodd  12980  qnumdenbi  12996  nn0sqdcq  13012  sqrtrirr  13013  phiprmpw  13028  eulerthlema  13036  fermltl  13040  prmdiveq  13042  modprm0  13061  pythagtriplem1  13072  pythagtriplem12  13082  pythagtriplem14  13084  pythagtriplem15  13085  pythagtriplem16  13086  pythagtriplem17  13087  pythagtriplem19  13089  pcpremul  13100  pcneg  13132  pcgcd  13136  pc2dvds  13137  pcaddlem  13146  pcprod  13153  fldivp1  13155  pcbc  13158  prmpwdvds  13162  pockthlem  13163  mul4sqlem  13200  4sqlem11  13208  4sqlem12  13209  4sqlem17  13214  ballotfilemrv  13320  ballotfilemfg  13326  ballotfilemfrc  13327  ballotfilemrinv0  13333  ctiunctlemfo  13387  ressval3d  13484  resseqnbasd  13485  imasival  13685  qusval  13702  plusfeqg  13742  sgrp1  13784  idmhm  13834  resmhm2  13853  mhmeql  13857  grppropstrg  13882  grpinvinv  13930  grp1  13969  imasgrp2  13971  mulgnngzsum  13988  mulginvcom  14008  mulgnndir  14012  mulgdir  14015  mulgneg2  14017  mulgnnass  14018  mulgass  14020  mulgsubdir  14023  trivsubgd  14061  nmzsubg  14071  qussub  14098  idghm  14120  cntzsubm  14169  cntzsubg  14170  ablinvadd  14203  ablsub2inv  14204  eqgabl  14223  gzsumgsum  14244  gsump1  14246  gsummptfidmsplit  14253  gsumconstcmn  14265  gsum2dfilem2  14271  prdsval  14279  mgpplusgg  14327  mgpbasg  14330  mgpscag  14332  mgptsetg  14333  mgpdsg  14335  mgpress  14336  srgpcomp  14400  srgpcompp  14401  ringo2times  14439  ring1eq0  14459  ring1  14470  opprmulfvalg  14483  crngoppr  14485  opprsllem  14487  oppr1g  14496  opprunitd  14525  rdivmuldivd  14559  rhmunitinv  14593  scafeqg  14753  lmodvsubval2  14787  lmodsubdi  14789  rmodislmod  14796  sralemg  14883  sraipg  14889  crng2idl  14976  cnfldmulg  15021  cnfldexp  15022  cnfldui  15032  mulgrhm2  15053  zrhrhmb  15065  zlmvscag  15076  znval2  15081  znbaslemnn  15082  znunit  15102  psrval  15160  psrmulrg  15195  psrgrp  15204  psrneg  15206  psrass1fi  15210  psrdifi  15211  psrdirfi  15212  mplsubgfileminv  15233  restuni2  15420  lmfval  15436  cnfval  15437  cnpfval  15438  txtopon  15505  txcnp  15514  upxp  15515  txrest  15519  cnmptcom  15541  bl2in  15646  xblss2  15648  isxms2  15695  setsmsdsg  15723  setsmstsetg  15724  metss  15737  resubmet  15799  expcn  15812  cncfcncntop  15836  dvidlemap  15934  dvidrelem  15935  dvidsslem  15936  dvcnp2cntop  15942  dvcoapbr  15950  dvcjbr  15951  dvexp  15954  dvexp2  15955  dvrecap  15956  plyaddlem1  15990  plymullem1  15991  plycolemc  16001  plycjlemc  16003  dvply1  16008  efimpi  16063  tangtx  16082  logdivlti  16128  logfac  16143  cxpexprp  16145  rpcxpsub  16158  rpabscxpbnd  16192  rprelogbdiv  16210  binom4  16236  log2tlbndlog2  16237  birthdaylem2  16243  pellexlem2  16247  prmorcht  16299  mpodvdsmulf1o  16301  0sgmppw  16304  chtqleppi  16311  chtublem  16312  pcbcctr  16320  bcmono  16321  bcp1ctr  16323  bclbnd  16324  bposlem3  16330  bposlem9  16336  lgslem1  16341  lgsmod  16367  lgsdilem  16368  lgsdi  16378  lgsne0  16379  lgsdirnn0  16388  lgsdinn0  16389  lgseisenlem2  16412  lgseisenlem3  16413  lgsquadlem2  16419  lgsquadlem3  16420  lgsquad2lem1  16422  lgsquad3  16425  2lgslem3  16442  2lgsoddprmlem2  16447  2sqlem4  16459  basvtxval2dom  16497  edgfiedgval2dom  16498  setsvtx  16514  ushgredgedgloop  16691  usgr1vr  16711  wlkres  16842  clwwlkccatlem  16863  trlsegvdegfi  16930  eupth2lem3lem2fi  16932  eupth2lem3lem6fi  16934  eupth2lem3lem4fi  16936  depindlem3  16971  bj-charfundcALT  17057  pw1ndom3lem  17241  pw1ndom3  17242  sssneq  17254  0nninf  17270  nnnninfex  17288  nninfnfiinf  17289  repiecele0  17298  trilpolemisumle  17311  qdiff  17322