Theorem eqtr4d 2213

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 2183	. 2 |- ( ph -> B = C )
4	1, 3	eqtrd 2210	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  3eqtr2d  2216  3eqtr2rd  2217  3eqtr4d  2220  3eqtr4rd  2221  3eqtr4a  2236  sbnfc2  3117  ifsbdc  3546  ifeq1dadc  3564  ifeq2dadc  3565  eqifdc  3569  ifnotdc  3571  ifandc  3572  ifordc  3573  onsucuni2  4563  relop  4777  riinint  4888  iotauni  5190  fniinfv  5574  fsn2  5690  fmptapd  5707  fconst2g  5731  fniunfv  5762  ofres  6096  ofco  6100  frecsuclem  6406  frecrdg  6408  oasuc  6464  nnacom  6484  nnaass  6485  nndi  6486  nnmass  6487  nnmsucr  6488  nnmcom  6489  funresdfunsndc  6506  uniqs2  6594  en1bg  6799  fundmen  6805  1domsn  6818  mapxpen  6847  xpmapenlem  6848  phplem4dom  6861  en2eqpr  6906  sbthlemi5  6959  omp1eomlem  7092  difinfsnlem  7097  ctmlemr  7106  ctssdccl  7109  ctssdc  7111  infnninf  7121  infnninfOLD  7122  nnnninfeq  7125  exmidonfinlem  7191  exmidmotap  7259  addcmpblnq  7365  distrnqg  7385  ltexnqq  7406  addcmpblnq0  7441  nqnq0a  7452  nqnq0m  7453  nq0m0r  7454  nq0a0  7455  nnanq0  7456  distrnq0  7457  prarloclemlo  7492  prarloclemcalc  7500  genpassl  7522  genpassu  7523  ltsosr  7762  0idsr  7765  1idsr  7766  mulextsr1lem  7778  cnegex  8134  subsub3  8188  subadd4  8200  mulneg12  8353  mulsub  8357  apreap  8543  cru  8558  recextlem1  8607  cju  8917  halfaddsub  9152  nn0supp  9227  nneo  9355  zeo2  9358  uzin  9559  xaddcom  9860  xaddass  9868  xleaddadd  9886  iccf1o  10003  fzsuc2  10078  flqeqceilz  10317  zmod1congr  10340  modqcyc  10358  modqcyc2  10359  modqaddabs  10361  modqmul1  10376  modqaddmulmod  10390  addmodlteq  10397  frec2uzrdg  10408  frecuzrdgsuctlem  10422  seq3val  10457  seqvalcd  10458  seq3fveq2  10468  seq3split  10478  seq3distr  10512  ser0f  10514  expp1  10526  mulexp  10558  mulexpzap  10559  expadd  10561  expaddzap  10563  expmul  10564  expmulzap  10565  expsubap  10567  expdivap  10570  subsq  10626  mulbinom2  10636  binom3  10637  bernneq  10640  modqexp  10646  nn0opthd  10701  faclbnd  10720  faclbnd6  10723  bccmpl  10733  bcp1n  10740  zfz1isolemiso  10818  seq3coll  10821  shftval2  10834  shftval4  10836  seq3shft  10846  crre  10865  remim  10868  remullem  10879  cjexp  10901  cnrecnv  10918  resqrexlemlo  11021  resqrexlemcalc1  11022  resqrexlemcalc2  11023  resqrexlemcalc3  11024  resqrexlemnm  11026  rsqrmo  11035  abscj  11060  absid  11079  absre  11085  recvalap  11105  maxabsle  11212  maxltsup  11226  2zsupmax  11233  minabs  11243  bdtrilem  11246  bdtri  11247  2zinfmin  11250  xrmaxiflemab  11254  xrmaxiflemcom  11256  xrmaxadd  11268  xrbdtri  11283  iooinsup  11284  climaddc1  11336  climmulc2  11338  climsubc1  11339  climsubc2  11340  climcvg1nlem  11356  summodclem3  11387  zsumdc  11391  isum  11392  isumz  11396  isumss  11398  fisumss  11399  fsum3cvg2  11401  fsumadd  11413  isummulc2  11433  sumsplitdc  11439  fsum2dlemstep  11441  fisumcom2  11445  fisum0diag2  11454  fsumconst  11461  telfsumo  11473  fsumparts  11477  fsumrelem  11478  binomlem  11490  isumshft  11497  isumsplit  11498  arisum  11505  arisum2  11506  trireciplem  11507  geolim2  11519  geo2sum  11521  0.999...  11528  cvgratz  11539  mertensabs  11544  clim2prod  11546  prodf1f  11550  prodmodclem2a  11583  zproddc  11586  iprodap  11587  iprodap0  11589  fprodseq  11590  prod1dc  11593  prodssdc  11596  fprod2dlemstep  11629  fprodcom2fi  11633  fproddivap  11637  ef0lem  11667  efval2  11672  ege2le3  11678  efaddlem  11681  efsub  11688  eftlub  11697  efsep  11698  tanval3ap  11721  efi4p  11724  sinneg  11733  sinmul  11751  sincossq  11755  cos2t  11757  demoivreALT  11780  eirraplem  11783  dvdsmodexp  11801  odd2np1  11877  omoe  11900  divalglemex  11926  divalglemeuneg  11927  divalgmod  11931  flodddiv4  11938  gcdneg  11982  gcdaddm  11984  modgcd  11991  bezoutlemnewy  11996  gcdass  12015  gcdmultiple  12020  algrp1  12045  lcmneg  12073  lcmgcdeq  12082  lcmass  12084  cncongr2  12103  prmexpb  12150  sqrt2irr  12161  2sqpwodd  12175  qnumdenbi  12191  phiprmpw  12221  eulerthlema  12229  fermltl  12233  prmdiveq  12235  modprm0  12253  pythagtriplem1  12264  pythagtriplem12  12274  pythagtriplem14  12276  pythagtriplem15  12277  pythagtriplem16  12278  pythagtriplem17  12279  pythagtriplem19  12281  pcpremul  12292  pcneg  12323  pcgcd  12327  pc2dvds  12328  pcaddlem  12337  pcprod  12343  fldivp1  12345  pcbc  12348  prmpwdvds  12352  pockthlem  12353  mul4sqlem  12390  ctiunctlemfo  12439  strslfv3  12507  ressval3d  12530  resseqnbasd  12531  imasival  12726  qusval  12743  plusfeqg  12782  sgrp1  12815  idmhm  12859  mhmeql  12875  grppropstrg  12894  grpinvinv  12936  grp1  12975  mulginvcom  13006  mulgnndir  13010  mulgdir  13013  mulgneg2  13015  mulgnnass  13016  mulgass  13018  mulgsubdir  13021  trivsubgd  13058  nmzsubg  13068  ablinvadd  13111  ablsub2inv  13112  mgpplusgg  13132  mgpbasg  13134  mgpscag  13135  mgptsetg  13136  mgpdsg  13138  mgpress  13139  srgpcomp  13171  srgpcompp  13172  rngo2times  13209  ring1eq0  13223  ring1  13234  opprmulfvalg  13240  crngoppr  13242  opprsllem  13244  oppr1g  13250  opprunitd  13277  rdivmuldivd  13311  scafeqg  13396  cnfldmulg  13440  cnfldexp  13441  restuni2  13647  lmfval  13662  cnfval  13664  cnpfval  13665  txtopon  13732  txcnp  13741  upxp  13742  txrest  13746  cnmptcom  13768  bl2in  13873  xblss2  13875  isxms2  13922  setsmsdsg  13950  setsmstsetg  13951  metss  13964  resubmet  14018  cncfcncntop  14050  dvidlemap  14130  dvcnp2cntop  14133  dvcoapbr  14141  dvcjbr  14142  dvexp  14145  dvexp2  14146  dvrecap  14147  efimpi  14210  tangtx  14229  logdivlti  14272  cxpexprp  14286  rpcxpsub  14299  rpabscxpbnd  14329  rprelogbdiv  14345  binom4  14367  lgslem1  14371  lgsmod  14397  lgsdilem  14398  lgsdi  14408  lgsne0  14409  lgsdirnn0  14418  lgsdinn0  14419  lgseisenlem2  14421  2lgsoddprmlem2  14424  2sqlem4  14435  bj-charfundcALT  14531  sssneq  14721  0nninf  14723  trilpolemisumle  14756