Theorem eqtr4d 2206

Description: An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)

Hypotheses

Ref	Expression
eqtr4d.1	|- ( ph -> A = B )
eqtr4d.2	|- ( ph -> C = B )

Assertion

Ref	Expression
eqtr4d	|- ( ph -> A = C )

Proof of Theorem eqtr4d

Step	Hyp	Ref	Expression
1		eqtr4d.1	. 2 |- ( ph -> A = B )
2		eqtr4d.2	. . 3 |- ( ph -> C = B )
3	2	eqcomd 2176	. 2 |- ( ph -> B = C )
4	1, 3	eqtrd 2203	1 |- ( ph -> A = C )

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  3538  ifeq1dadc  3556  eqifdc  3560  ifnotdc  3562  ifandc  3563  ifordc  3564  onsucuni2  4548  relop  4761  riinint  4872  iotauni  5172  fniinfv  5554  fsn2  5670  fmptapd  5687  fconst2g  5711  fniunfv  5741  ofres  6075  ofco  6079  frecsuclem  6385  frecrdg  6387  oasuc  6443  nnacom  6463  nnaass  6464  nndi  6465  nnmass  6466  nnmsucr  6467  nnmcom  6468  funresdfunsndc  6485  uniqs2  6573  en1bg  6778  fundmen  6784  1domsn  6797  mapxpen  6826  xpmapenlem  6827  phplem4dom  6840  en2eqpr  6885  sbthlemi5  6938  omp1eomlem  7071  difinfsnlem  7076  ctmlemr  7085  ctssdccl  7088  ctssdc  7090  infnninf  7100  infnninfOLD  7101  nnnninfeq  7104  exmidonfinlem  7170  addcmpblnq  7329  distrnqg  7349  ltexnqq  7370  addcmpblnq0  7405  nqnq0a  7416  nqnq0m  7417  nq0m0r  7418  nq0a0  7419  nnanq0  7420  distrnq0  7421  prarloclemlo  7456  prarloclemcalc  7464  genpassl  7486  genpassu  7487  ltsosr  7726  0idsr  7729  1idsr  7730  mulextsr1lem  7742  cnegex  8097  subsub3  8151  subadd4  8163  mulneg12  8316  mulsub  8320  apreap  8506  cru  8521  recextlem1  8569  cju  8877  halfaddsub  9112  nn0supp  9187  nneo  9315  zeo2  9318  uzin  9519  xaddcom  9818  xaddass  9826  xleaddadd  9844  iccf1o  9961  fzsuc2  10035  flqeqceilz  10274  zmod1congr  10297  modqcyc  10315  modqcyc2  10316  modqaddabs  10318  modqmul1  10333  modqaddmulmod  10347  addmodlteq  10354  frec2uzrdg  10365  frecuzrdgsuctlem  10379  seq3val  10414  seqvalcd  10415  seq3fveq2  10425  seq3split  10435  seq3distr  10469  ser0f  10471  expp1  10483  mulexp  10515  mulexpzap  10516  expadd  10518  expaddzap  10520  expmul  10521  expmulzap  10522  expsubap  10524  expdivap  10527  subsq  10582  mulbinom2  10592  binom3  10593  bernneq  10596  modqexp  10602  nn0opthd  10656  faclbnd  10675  faclbnd6  10678  bccmpl  10688  bcp1n  10695  zfz1isolemiso  10774  seq3coll  10777  shftval2  10790  shftval4  10792  seq3shft  10802  crre  10821  remim  10824  remullem  10835  cjexp  10857  cnrecnv  10874  resqrexlemlo  10977  resqrexlemcalc1  10978  resqrexlemcalc2  10979  resqrexlemcalc3  10980  resqrexlemnm  10982  rsqrmo  10991  abscj  11016  absid  11035  absre  11041  recvalap  11061  maxabsle  11168  maxltsup  11182  2zsupmax  11189  minabs  11199  bdtrilem  11202  bdtri  11203  2zinfmin  11206  xrmaxiflemab  11210  xrmaxiflemcom  11212  xrmaxadd  11224  xrbdtri  11239  iooinsup  11240  climaddc1  11292  climmulc2  11294  climsubc1  11295  climsubc2  11296  climcvg1nlem  11312  summodclem3  11343  zsumdc  11347  isum  11348  isumz  11352  isumss  11354  fisumss  11355  fsum3cvg2  11357  fsumadd  11369  isummulc2  11389  sumsplitdc  11395  fsum2dlemstep  11397  fisumcom2  11401  fisum0diag2  11410  fsumconst  11417  telfsumo  11429  fsumparts  11433  fsumrelem  11434  binomlem  11446  isumshft  11453  isumsplit  11454  arisum  11461  arisum2  11462  trireciplem  11463  geolim2  11475  geo2sum  11477  0.999...  11484  cvgratz  11495  mertensabs  11500  clim2prod  11502  prodf1f  11506  prodmodclem2a  11539  zproddc  11542  iprodap  11543  iprodap0  11545  fprodseq  11546  prod1dc  11549  prodssdc  11552  fprod2dlemstep  11585  fprodcom2fi  11589  fproddivap  11593  ef0lem  11623  efval2  11628  ege2le3  11634  efaddlem  11637  efsub  11644  eftlub  11653  efsep  11654  tanval3ap  11677  efi4p  11680  sinneg  11689  sinmul  11707  sincossq  11711  cos2t  11713  demoivreALT  11736  eirraplem  11739  dvdsmodexp  11757  odd2np1  11832  omoe  11855  divalglemex  11881  divalglemeuneg  11882  divalgmod  11886  flodddiv4  11893  gcdneg  11937  gcdaddm  11939  modgcd  11946  bezoutlemnewy  11951  gcdass  11970  gcdmultiple  11975  algrp1  12000  lcmneg  12028  lcmgcdeq  12037  lcmass  12039  cncongr2  12058  prmexpb  12105  sqrt2irr  12116  2sqpwodd  12130  qnumdenbi  12146  phiprmpw  12176  eulerthlema  12184  fermltl  12188  prmdiveq  12190  modprm0  12208  pythagtriplem1  12219  pythagtriplem12  12229  pythagtriplem14  12231  pythagtriplem15  12232  pythagtriplem16  12233  pythagtriplem17  12234  pythagtriplem19  12236  pcpremul  12247  pcneg  12278  pcgcd  12282  pc2dvds  12283  pcaddlem  12292  pcprod  12298  fldivp1  12300  pcbc  12303  prmpwdvds  12307  pockthlem  12308  mul4sqlem  12345  ctiunctlemfo  12394  strslfv3  12461  plusfeqg  12618  sgrp1  12651  idmhm  12692  mhmeql  12707  grpinvinv  12766  restuni2  12971  lmfval  12986  cnfval  12988  cnpfval  12989  txtopon  13056  txcnp  13065  upxp  13066  txrest  13070  cnmptcom  13092  bl2in  13197  xblss2  13199  isxms2  13246  setsmsdsg  13274  setsmstsetg  13275  metss  13288  resubmet  13342  cncfcncntop  13374  dvidlemap  13454  dvcnp2cntop  13457  dvcoapbr  13465  dvcjbr  13466  dvexp  13469  dvexp2  13470  dvrecap  13471  efimpi  13534  tangtx  13553  logdivlti  13596  cxpexprp  13610  rpcxpsub  13623  rpabscxpbnd  13653  rprelogbdiv  13669  binom4  13691  lgslem1  13695  lgsmod  13721  lgsdilem  13722  lgsdi  13732  lgsne0  13733  lgsdirnn0  13742  lgsdinn0  13743  2sqlem4  13748  bj-charfundcALT  13844  sssneq  14035  0nninf  14037  trilpolemisumle  14070