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  6681  frecrdg  6683  oasuc  6741  nnacom  6761  nnaass  6762  nndi  6763  nnmass  6764  nnmsucr  6765  nnmcom  6766  funresdfunsndc  6783  uniqs2  6873  en1bg  7091  fundmen  7098  1dom1el  7111  1domsn  7119  pw2f1odclem  7138  mapxpen  7152  xpmapenlem  7153  mapunen  7155  phplem4dom  7167  en2eqpr  7218  sbthlemi5  7283  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  9630  nneo  9760  zeo2  9763  uzin  9971  xaddcom  10280  xaddass  10288  xleaddadd  10306  iccf1o  10424  fzsuc2  10503  fldiv4lem1div2uz2  10762  flqeqceilz  10776  zmod1congr  10799  modqcyc  10817  modqcyc2  10818  modqaddabs  10820  modqmul1  10835  modqaddmulmod  10849  addmodlteq  10856  frec2uzrdg  10867  frecuzrdgsuctlem  10881  seq3val  10918  seqvalcd  10919  seq3fveq2  10933  seqfveq2g  10935  seq3split  10946  seqsplitg  10947  seqf1oglem2a  10976  seqf1oglem2  10978  seqfeq4g  10989  seq3distr  10990  ser0f  10992  expp1  11004  mulexp  11036  mulexpzap  11037  expadd  11039  expaddzap  11041  expmul  11042  expmulzap  11043  expsubap  11045  expdivap  11048  subsq  11104  mulbinom2  11114  binom3  11115  bernneq  11119  modqexp  11125  nn0opthd  11182  faclbnd  11201  faclbnd6  11204  bccmpl  11214  bcp1n  11221  hashfibclem  11304  hashfibc  11305  hashf1lem1  11307  hashf1  11309  zfz1isolemiso  11313  seq3coll  11316  hashtpglem  11320  ccatsymb  11392  ccatval1lsw  11394  ccatass  11398  eqs1  11418  lswccats1fst  11434  swrdsb0eq  11459  swrdsbslen  11460  swrds1  11462  ccatswrd  11464  pfxres  11475  ccatpfx  11495  pfxpfx  11502  cats1un  11515  swrdccatin1  11519  pfxccatin12  11527  swrdccat  11529  pfxccat3a  11532  swrdccat3b  11534  shftval2  11613  shftval4  11615  seq3shft  11625  crre  11644  remim  11647  remullem  11658  cjexp  11680  sq01  11682  cnrecnv  11698  resqrexlemlo  11801  resqrexlemcalc1  11802  resqrexlemcalc2  11803  resqrexlemcalc3  11804  resqrexlemnm  11806  rsqrmo  11815  abscj  11840  absid  11859  absre  11866  recvalap  11886  maxabsle  11993  maxltsup  12007  2zsupmax  12015  minabs  12026  bdtrilem  12030  bdtri  12031  2zinfmin  12034  xrmaxiflemab  12038  xrmaxiflemcom  12040  xrmaxadd  12052  xrbdtri  12067  iooinsup  12068  climaddc1  12120  climmulc2  12122  climsubc1  12123  climsubc2  12124  climcvg1nlem  12140  summodclem3  12172  zsumdc  12176  isum  12177  isumz  12181  isumss  12183  fisumss  12184  fsum3cvg2  12186  fsumadd  12198  isummulc2  12218  sumsplitdc  12224  fsum2dlemstep  12226  fisumcom2  12230  fisum0diag2  12239  fsumconst  12246  telfsumo  12258  fsumparts  12262  fsumrelem  12263  binomlem  12275  isumshft  12282  isumsplit  12283  arisum  12290  arisum2  12291  trireciplem  12292  geolim2  12304  geo2sum  12306  0.999...  12313  cvgratz  12324  mertensabs  12329  clim2prod  12331  prodf1f  12335  prodmodclem2a  12368  zproddc  12371  iprodap  12372  iprodap0  12374  fprodseq  12375  prod1dc  12378  prodssdc  12381  fprod2dlemstep  12414  fprodcom2fi  12418  fproddivap  12422  ef0lem  12452  efval2  12457  ege2le3  12463  efaddlem  12466  efsub  12473  eftlub  12482  efsep  12483  tanval3ap  12506  efi4p  12509  sinneg  12518  sinmul  12536  sincossq  12540  cos2t  12542  demoivreALT  12566  eirraplem  12569  dvdsmodexp  12587  odd2np1  12665  omoe  12688  divalglemex  12714  divalglemeuneg  12715  divalgmod  12719  flodddiv4  12728  bitsp1  12743  bitsinv1lem  12753  bitsinv1  12754  gcdneg  12784  gcdaddm  12786  modgcd  12793  bezoutlemnewy  12798  gcdass  12817  gcdmultiple  12822  nninfctlemfo  12842  algrp1  12849  lcmneg  12877  lcmgcdeq  12886  lcmass  12888  cncongr2  12907  prmexpb  12955  sqrt2irr  12966  2sqpwodd  12981  qnumdenbi  12997  nn0sqdcq  13013  sqrtrirr  13014  phiprmpw  13029  eulerthlema  13037  fermltl  13041  prmdiveq  13043  modprm0  13062  pythagtriplem1  13073  pythagtriplem12  13083  pythagtriplem14  13085  pythagtriplem15  13086  pythagtriplem16  13087  pythagtriplem17  13088  pythagtriplem19  13090  pcpremul  13101  pcneg  13133  pcgcd  13137  pc2dvds  13138  pcaddlem  13147  pcprod  13154  fldivp1  13156  pcbc  13159  prmpwdvds  13163  pockthlem  13164  mul4sqlem  13201  4sqlem11  13209  4sqlem12  13210  4sqlem17  13215  ballotfilemrv  13321  ballotfilemfg  13327  ballotfilemfrc  13328  ballotfilemrinv0  13334  ctiunctlemfo  13388  ressval3d  13485  resseqnbasd  13486  imasival  13686  qusval  13703  plusfeqg  13743  sgrp1  13785  idmhm  13835  resmhm2  13854  mhmeql  13858  grppropstrg  13883  grpinvinv  13931  grp1  13970  imasgrp2  13972  mulgnngzsum  13989  mulginvcom  14009  mulgnndir  14013  mulgdir  14016  mulgneg2  14018  mulgnnass  14019  mulgass  14021  mulgsubdir  14024  trivsubgd  14062  nmzsubg  14072  qussub  14099  idghm  14121  cntzsubm  14170  cntzsubg  14171  ablinvadd  14204  ablsub2inv  14205  eqgabl  14224  gzsumgsum  14245  gsump1  14247  gsummptfidmsplit  14254  gsumconstcmn  14266  gsum2dfilem2  14272  prdsval  14280  mgpplusgg  14328  mgpbasg  14331  mgpscag  14333  mgptsetg  14334  mgpdsg  14336  mgpress  14337  srgpcomp  14401  srgpcompp  14402  ringo2times  14440  ring1eq0  14460  ring1  14471  opprmulfvalg  14484  crngoppr  14486  opprsllem  14488  oppr1g  14497  opprunitd  14526  rdivmuldivd  14560  rhmunitinv  14594  scafeqg  14754  lmodvsubval2  14788  lmodsubdi  14790  rmodislmod  14797  sralemg  14884  sraipg  14890  crng2idl  14977  cnfldmulg  15022  cnfldexp  15023  cnfldui  15033  mulgrhm2  15054  zrhrhmb  15066  zlmvscag  15077  znval2  15082  znbaslemnn  15083  znunit  15103  psrval  15159  psrmulrg  15186  psrgrp  15195  psrneg  15197  psrass1fi  15201  psrdifi  15202  psrdirfi  15203  mplval2g  15211  restuni2  15403  lmfval  15419  cnfval  15420  cnpfval  15421  txtopon  15488  txcnp  15497  upxp  15498  txrest  15502  cnmptcom  15524  bl2in  15629  xblss2  15631  isxms2  15678  setsmsdsg  15706  setsmstsetg  15707  metss  15720  resubmet  15782  expcn  15795  cncfcncntop  15819  dvidlemap  15917  dvidrelem  15918  dvidsslem  15919  dvcnp2cntop  15925  dvcoapbr  15933  dvcjbr  15934  dvexp  15937  dvexp2  15938  dvrecap  15939  plyaddlem1  15973  plymullem1  15974  plycolemc  15984  plycjlemc  15986  dvply1  15991  efimpi  16046  tangtx  16065  logdivlti  16111  logfac  16126  cxpexprp  16128  rpcxpsub  16141  rpabscxpbnd  16175  rprelogbdiv  16193  binom4  16219  log2tlbndlog2  16220  birthdaylem2  16226  pellexlem2  16230  prmorcht  16282  mpodvdsmulf1o  16284  0sgmppw  16287  chtqleppi  16294  chtublem  16295  pcbcctr  16303  bcmono  16304  bcp1ctr  16306  bclbnd  16307  bposlem3  16313  bposlem9  16319  lgslem1  16324  lgsmod  16350  lgsdilem  16351  lgsdi  16361  lgsne0  16362  lgsdirnn0  16371  lgsdinn0  16372  lgseisenlem2  16395  lgseisenlem3  16396  lgsquadlem2  16402  lgsquadlem3  16403  lgsquad2lem1  16405  lgsquad3  16408  2lgslem3  16425  2lgsoddprmlem2  16430  2sqlem4  16442  basvtxval2dom  16480  edgfiedgval2dom  16481  setsvtx  16497  ushgredgedgloop  16674  usgr1vr  16694  wlkres  16825  clwwlkccatlem  16846  trlsegvdegfi  16913  eupth2lem3lem2fi  16915  eupth2lem3lem6fi  16917  eupth2lem3lem4fi  16919  depindlem3  16954  bj-charfundcALT  17040  pw1ndom3lem  17224  pw1ndom3  17225  sssneq  17237  0nninf  17253  nnnninfex  17271  nninfnfiinf  17272  repiecele0  17281  trilpolemisumle  17294  qdiff  17305