Theorem eqtr4d 2206

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

Syntax hints:   → wi 4   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  3eqtr2d  2209  3eqtr2rd  2210  3eqtr4d  2213  3eqtr4rd  2214  3eqtr4a  2229  sbnfc2  3109  ifsbdc  3537  ifeq1dadc  3555  eqifdc  3559  ifnotdc  3561  ifandc  3562  onsucuni2  4546  relop  4759  riinint  4870  iotauni  5170  fniinfv  5552  fsn2  5668  fmptapd  5685  fconst2g  5709  fniunfv  5739  ofres  6073  ofco  6077  frecsuclem  6383  frecrdg  6385  oasuc  6441  nnacom  6461  nnaass  6462  nndi  6463  nnmass  6464  nnmsucr  6465  nnmcom  6466  funresdfunsndc  6483  uniqs2  6570  en1bg  6775  fundmen  6781  1domsn  6794  mapxpen  6823  xpmapenlem  6824  phplem4dom  6837  en2eqpr  6882  sbthlemi5  6935  omp1eomlem  7068  difinfsnlem  7073  ctmlemr  7082  ctssdccl  7085  ctssdc  7087  infnninf  7097  infnninfOLD  7098  nnnninfeq  7101  exmidonfinlem  7159  addcmpblnq  7318  distrnqg  7338  ltexnqq  7359  addcmpblnq0  7394  nqnq0a  7405  nqnq0m  7406  nq0m0r  7407  nq0a0  7408  nnanq0  7409  distrnq0  7410  prarloclemlo  7445  prarloclemcalc  7453  genpassl  7475  genpassu  7476  ltsosr  7715  0idsr  7718  1idsr  7719  mulextsr1lem  7731  cnegex  8086  subsub3  8140  subadd4  8152  mulneg12  8305  mulsub  8309  apreap  8495  cru  8510  recextlem1  8558  cju  8866  halfaddsub  9101  nn0supp  9176  nneo  9304  zeo2  9307  uzin  9508  xaddcom  9807  xaddass  9815  xleaddadd  9833  iccf1o  9950  fzsuc2  10024  flqeqceilz  10263  zmod1congr  10286  modqcyc  10304  modqcyc2  10305  modqaddabs  10307  modqmul1  10322  modqaddmulmod  10336  addmodlteq  10343  frec2uzrdg  10354  frecuzrdgsuctlem  10368  seq3val  10403  seqvalcd  10404  seq3fveq2  10414  seq3split  10424  seq3distr  10458  ser0f  10460  expp1  10472  mulexp  10504  mulexpzap  10505  expadd  10507  expaddzap  10509  expmul  10510  expmulzap  10511  expsubap  10513  expdivap  10516  subsq  10571  mulbinom2  10581  binom3  10582  bernneq  10585  modqexp  10591  nn0opthd  10645  faclbnd  10664  faclbnd6  10667  bccmpl  10677  bcp1n  10684  zfz1isolemiso  10763  seq3coll  10766  shftval2  10779  shftval4  10781  seq3shft  10791  crre  10810  remim  10813  remullem  10824  cjexp  10846  cnrecnv  10863  resqrexlemlo  10966  resqrexlemcalc1  10967  resqrexlemcalc2  10968  resqrexlemcalc3  10969  resqrexlemnm  10971  rsqrmo  10980  abscj  11005  absid  11024  absre  11030  recvalap  11050  maxabsle  11157  maxltsup  11171  2zsupmax  11178  minabs  11188  bdtrilem  11191  bdtri  11192  2zinfmin  11195  xrmaxiflemab  11199  xrmaxiflemcom  11201  xrmaxadd  11213  xrbdtri  11228  iooinsup  11229  climaddc1  11281  climmulc2  11283  climsubc1  11284  climsubc2  11285  climcvg1nlem  11301  summodclem3  11332  zsumdc  11336  isum  11337  isumz  11341  isumss  11343  fisumss  11344  fsum3cvg2  11346  fsumadd  11358  isummulc2  11378  sumsplitdc  11384  fsum2dlemstep  11386  fisumcom2  11390  fisum0diag2  11399  fsumconst  11406  telfsumo  11418  fsumparts  11422  fsumrelem  11423  binomlem  11435  isumshft  11442  isumsplit  11443  arisum  11450  arisum2  11451  trireciplem  11452  geolim2  11464  geo2sum  11466  0.999...  11473  cvgratz  11484  mertensabs  11489  clim2prod  11491  prodf1f  11495  prodmodclem2a  11528  zproddc  11531  iprodap  11532  iprodap0  11534  fprodseq  11535  prod1dc  11538  prodssdc  11541  fprod2dlemstep  11574  fprodcom2fi  11578  fproddivap  11582  ef0lem  11612  efval2  11617  ege2le3  11623  efaddlem  11626  efsub  11633  eftlub  11642  efsep  11643  tanval3ap  11666  efi4p  11669  sinneg  11678  sinmul  11696  sincossq  11700  cos2t  11702  demoivreALT  11725  eirraplem  11728  dvdsmodexp  11746  odd2np1  11821  omoe  11844  divalglemex  11870  divalglemeuneg  11871  divalgmod  11875  flodddiv4  11882  gcdneg  11926  gcdaddm  11928  modgcd  11935  bezoutlemnewy  11940  gcdass  11959  gcdmultiple  11964  algrp1  11989  lcmneg  12017  lcmgcdeq  12026  lcmass  12028  cncongr2  12047  prmexpb  12094  sqrt2irr  12105  2sqpwodd  12119  qnumdenbi  12135  phiprmpw  12165  eulerthlema  12173  fermltl  12177  prmdiveq  12179  modprm0  12197  pythagtriplem1  12208  pythagtriplem12  12218  pythagtriplem14  12220  pythagtriplem15  12221  pythagtriplem16  12222  pythagtriplem17  12223  pythagtriplem19  12225  pcpremul  12236  pcneg  12267  pcgcd  12271  pc2dvds  12272  pcaddlem  12281  pcprod  12287  fldivp1  12289  pcbc  12292  prmpwdvds  12296  pockthlem  12297  mul4sqlem  12334  ctiunctlemfo  12383  strslfv3  12450  plusfeqg  12607  sgrp1  12640  idmhm  12681  mhmeql  12696  restuni2  12932  lmfval  12947  cnfval  12949  cnpfval  12950  txtopon  13017  txcnp  13026  upxp  13027  txrest  13031  cnmptcom  13053  bl2in  13158  xblss2  13160  isxms2  13207  setsmsdsg  13235  setsmstsetg  13236  metss  13249  resubmet  13303  cncfcncntop  13335  dvidlemap  13415  dvcnp2cntop  13418  dvcoapbr  13426  dvcjbr  13427  dvexp  13430  dvexp2  13431  dvrecap  13432  efimpi  13495  tangtx  13514  logdivlti  13557  cxpexprp  13571  rpcxpsub  13584  rpabscxpbnd  13614  rprelogbdiv  13630  binom4  13652  lgslem1  13656  lgsmod  13682  lgsdilem  13683  lgsdi  13693  lgsne0  13694  lgsdirnn0  13703  lgsdinn0  13704  2sqlem4  13709  bj-charfundcALT  13806  sssneq  13997  0nninf  13999  trilpolemisumle  14032