Theorem eqtr4d 2225

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

Syntax hints:   → wi 4   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-cleq 2182

This theorem is referenced by:  3eqtr2d  2228  3eqtr2rd  2229  3eqtr4d  2232  3eqtr4rd  2233  3eqtr4a  2248  sbnfc2  3132  ifsbdc  3561  ifeq1dadc  3579  ifeq2dadc  3580  eqifdc  3584  ifnotdc  3586  ifandc  3587  ifordc  3588  onsucuni2  4581  relop  4795  riinint  4906  iotauni  5208  fniinfv  5595  fsn2  5711  fmptapd  5728  fconst2g  5752  fniunfv  5784  ofres  6121  ofco  6125  frecsuclem  6431  frecrdg  6433  oasuc  6489  nnacom  6509  nnaass  6510  nndi  6511  nnmass  6512  nnmsucr  6513  nnmcom  6514  funresdfunsndc  6531  uniqs2  6621  en1bg  6826  fundmen  6832  1domsn  6845  pw2f1odclem  6862  mapxpen  6876  xpmapenlem  6877  phplem4dom  6890  en2eqpr  6935  sbthlemi5  6990  omp1eomlem  7123  difinfsnlem  7128  ctmlemr  7137  ctssdccl  7140  ctssdc  7142  infnninf  7152  infnninfOLD  7153  nnnninfeq  7156  exmidonfinlem  7222  exmidmotap  7290  addcmpblnq  7396  distrnqg  7416  ltexnqq  7437  addcmpblnq0  7472  nqnq0a  7483  nqnq0m  7484  nq0m0r  7485  nq0a0  7486  nnanq0  7487  distrnq0  7488  prarloclemlo  7523  prarloclemcalc  7531  genpassl  7553  genpassu  7554  ltsosr  7793  0idsr  7796  1idsr  7797  mulextsr1lem  7809  cnegex  8165  subsub3  8219  subadd4  8231  mulneg12  8384  mulsub  8388  apreap  8574  cru  8589  recextlem1  8638  cju  8948  halfaddsub  9183  nn0supp  9258  nneo  9386  zeo2  9389  uzin  9590  xaddcom  9891  xaddass  9899  xleaddadd  9917  iccf1o  10034  fzsuc2  10109  flqeqceilz  10349  zmod1congr  10372  modqcyc  10390  modqcyc2  10391  modqaddabs  10393  modqmul1  10408  modqaddmulmod  10422  addmodlteq  10429  frec2uzrdg  10440  frecuzrdgsuctlem  10454  seq3val  10489  seqvalcd  10490  seq3fveq2  10500  seq3split  10510  seq3distr  10544  ser0f  10546  expp1  10558  mulexp  10590  mulexpzap  10591  expadd  10593  expaddzap  10595  expmul  10596  expmulzap  10597  expsubap  10599  expdivap  10602  subsq  10658  mulbinom2  10668  binom3  10669  bernneq  10672  modqexp  10678  nn0opthd  10734  faclbnd  10753  faclbnd6  10756  bccmpl  10766  bcp1n  10773  zfz1isolemiso  10851  seq3coll  10854  shftval2  10867  shftval4  10869  seq3shft  10879  crre  10898  remim  10901  remullem  10912  cjexp  10934  cnrecnv  10951  resqrexlemlo  11054  resqrexlemcalc1  11055  resqrexlemcalc2  11056  resqrexlemcalc3  11057  resqrexlemnm  11059  rsqrmo  11068  abscj  11093  absid  11112  absre  11118  recvalap  11138  maxabsle  11245  maxltsup  11259  2zsupmax  11266  minabs  11276  bdtrilem  11279  bdtri  11280  2zinfmin  11283  xrmaxiflemab  11287  xrmaxiflemcom  11289  xrmaxadd  11301  xrbdtri  11316  iooinsup  11317  climaddc1  11369  climmulc2  11371  climsubc1  11372  climsubc2  11373  climcvg1nlem  11389  summodclem3  11420  zsumdc  11424  isum  11425  isumz  11429  isumss  11431  fisumss  11432  fsum3cvg2  11434  fsumadd  11446  isummulc2  11466  sumsplitdc  11472  fsum2dlemstep  11474  fisumcom2  11478  fisum0diag2  11487  fsumconst  11494  telfsumo  11506  fsumparts  11510  fsumrelem  11511  binomlem  11523  isumshft  11530  isumsplit  11531  arisum  11538  arisum2  11539  trireciplem  11540  geolim2  11552  geo2sum  11554  0.999...  11561  cvgratz  11572  mertensabs  11577  clim2prod  11579  prodf1f  11583  prodmodclem2a  11616  zproddc  11619  iprodap  11620  iprodap0  11622  fprodseq  11623  prod1dc  11626  prodssdc  11629  fprod2dlemstep  11662  fprodcom2fi  11666  fproddivap  11670  ef0lem  11700  efval2  11705  ege2le3  11711  efaddlem  11714  efsub  11721  eftlub  11730  efsep  11731  tanval3ap  11754  efi4p  11757  sinneg  11766  sinmul  11784  sincossq  11788  cos2t  11790  demoivreALT  11813  eirraplem  11816  dvdsmodexp  11834  odd2np1  11910  omoe  11933  divalglemex  11959  divalglemeuneg  11960  divalgmod  11964  flodddiv4  11971  gcdneg  12015  gcdaddm  12017  modgcd  12024  bezoutlemnewy  12029  gcdass  12048  gcdmultiple  12053  algrp1  12078  lcmneg  12106  lcmgcdeq  12115  lcmass  12117  cncongr2  12136  prmexpb  12183  sqrt2irr  12194  2sqpwodd  12208  qnumdenbi  12224  phiprmpw  12254  eulerthlema  12262  fermltl  12266  prmdiveq  12268  modprm0  12286  pythagtriplem1  12297  pythagtriplem12  12307  pythagtriplem14  12309  pythagtriplem15  12310  pythagtriplem16  12311  pythagtriplem17  12312  pythagtriplem19  12314  pcpremul  12325  pcneg  12357  pcgcd  12361  pc2dvds  12362  pcaddlem  12371  pcprod  12378  fldivp1  12380  pcbc  12383  prmpwdvds  12387  pockthlem  12388  mul4sqlem  12425  4sqlem11  12433  4sqlem12  12434  4sqlem17  12439  ctiunctlemfo  12490  strslfv3  12558  ressval3d  12584  resseqnbasd  12585  imasival  12783  qusval  12800  plusfeqg  12840  sgrp1  12874  idmhm  12921  resmhm2  12940  mhmeql  12944  grppropstrg  12964  grpinvinv  13011  grp1  13050  imasgrp2  13052  mulginvcom  13087  mulgnndir  13091  mulgdir  13094  mulgneg2  13096  mulgnnass  13097  mulgass  13099  mulgsubdir  13102  trivsubgd  13139  nmzsubg  13149  qussub  13176  idghm  13198  ablinvadd  13249  ablsub2inv  13250  eqgabl  13267  mgpplusgg  13278  mgpbasg  13280  mgpscag  13281  mgptsetg  13282  mgpdsg  13284  mgpress  13285  srgpcomp  13344  srgpcompp  13345  ringo2times  13382  ring1eq0  13400  ring1  13411  opprmulfvalg  13420  crngoppr  13422  opprsllem  13424  oppr1g  13432  opprunitd  13460  rdivmuldivd  13494  rhmunitinv  13528  scafeqg  13624  lmodvsubval2  13658  lmodsubdi  13660  rmodislmod  13667  sralemg  13754  sraipg  13760  crng2idl  13845  cnfldmulg  13879  cnfldexp  13880  mulgrhm2  13908  zrhrhmb  13919  zlmvscag  13929  znval2  13934  znbaslemnn  13935  psrval  13944  restuni2  14137  lmfval  14152  cnfval  14154  cnpfval  14155  txtopon  14222  txcnp  14231  upxp  14232  txrest  14236  cnmptcom  14258  bl2in  14363  xblss2  14365  isxms2  14412  setsmsdsg  14440  setsmstsetg  14441  metss  14454  resubmet  14508  cncfcncntop  14540  dvidlemap  14620  dvcnp2cntop  14623  dvcoapbr  14631  dvcjbr  14632  dvexp  14635  dvexp2  14636  dvrecap  14637  efimpi  14700  tangtx  14719  logdivlti  14762  cxpexprp  14776  rpcxpsub  14789  rpabscxpbnd  14819  rprelogbdiv  14835  binom4  14857  lgslem1  14862  lgsmod  14888  lgsdilem  14889  lgsdi  14899  lgsne0  14900  lgsdirnn0  14909  lgsdinn0  14910  lgseisenlem2  14912  2lgsoddprmlem2  14915  2sqlem4  14926  bj-charfundcALT  15022  1dom1el  15204  sssneq  15213  0nninf  15215  trilpolemisumle  15248