Theorem eqtr4d 2193

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

Syntax hints:   -> wi 4   = wceq 1335

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 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ext 2139

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

This theorem is referenced by:  3eqtr2d  2196  3eqtr2rd  2197  3eqtr4d  2200  3eqtr4rd  2201  3eqtr4a  2216  sbnfc2  3091  ifsbdc  3517  ifeq1dadc  3535  eqifdc  3539  ifandc  3541  onsucuni2  4522  relop  4735  riinint  4846  iotauni  5146  fniinfv  5525  fsn2  5640  fmptapd  5657  fconst2g  5681  fniunfv  5709  ofres  6043  ofco  6047  frecsuclem  6350  frecrdg  6352  oasuc  6408  nnacom  6428  nnaass  6429  nndi  6430  nnmass  6431  nnmsucr  6432  nnmcom  6433  funresdfunsndc  6450  uniqs2  6537  en1bg  6742  fundmen  6748  1domsn  6761  mapxpen  6790  xpmapenlem  6791  phplem4dom  6804  en2eqpr  6849  sbthlemi5  6902  omp1eomlem  7032  difinfsnlem  7037  ctmlemr  7046  ctssdccl  7049  ctssdc  7051  infnninf  7061  infnninfOLD  7062  nnnninfeq  7065  exmidonfinlem  7122  addcmpblnq  7281  distrnqg  7301  ltexnqq  7322  addcmpblnq0  7357  nqnq0a  7368  nqnq0m  7369  nq0m0r  7370  nq0a0  7371  nnanq0  7372  distrnq0  7373  prarloclemlo  7408  prarloclemcalc  7416  genpassl  7438  genpassu  7439  ltsosr  7678  0idsr  7681  1idsr  7682  mulextsr1lem  7694  cnegex  8047  subsub3  8101  subadd4  8113  mulneg12  8266  mulsub  8270  apreap  8456  cru  8471  recextlem1  8519  cju  8826  halfaddsub  9061  nn0supp  9136  nneo  9261  zeo2  9264  uzin  9465  xaddcom  9758  xaddass  9766  xleaddadd  9784  iccf1o  9901  fzsuc2  9974  flqeqceilz  10210  zmod1congr  10233  modqcyc  10251  modqcyc2  10252  modqaddabs  10254  modqmul1  10269  modqaddmulmod  10283  addmodlteq  10290  frec2uzrdg  10301  frecuzrdgsuctlem  10315  seq3val  10350  seqvalcd  10351  seq3fveq2  10361  seq3split  10371  seq3distr  10405  ser0f  10407  expp1  10419  mulexp  10451  mulexpzap  10452  expadd  10454  expaddzap  10456  expmul  10457  expmulzap  10458  expsubap  10460  expdivap  10463  subsq  10518  mulbinom2  10527  binom3  10528  bernneq  10531  modqexp  10537  nn0opthd  10589  faclbnd  10608  faclbnd6  10611  bccmpl  10621  bcp1n  10628  zfz1isolemiso  10703  seq3coll  10706  shftval2  10719  shftval4  10721  seq3shft  10731  crre  10750  remim  10753  remullem  10764  cjexp  10786  cnrecnv  10803  resqrexlemlo  10906  resqrexlemcalc1  10907  resqrexlemcalc2  10908  resqrexlemcalc3  10909  resqrexlemnm  10911  rsqrmo  10920  abscj  10945  absid  10964  absre  10970  recvalap  10990  maxabsle  11097  maxltsup  11111  2zsupmax  11118  minabs  11128  bdtrilem  11131  bdtri  11132  xrmaxiflemab  11137  xrmaxiflemcom  11139  xrmaxadd  11151  xrbdtri  11166  iooinsup  11167  climaddc1  11219  climmulc2  11221  climsubc1  11222  climsubc2  11223  climcvg1nlem  11239  summodclem3  11270  zsumdc  11274  isum  11275  isumz  11279  isumss  11281  fisumss  11282  fsum3cvg2  11284  fsumadd  11296  isummulc2  11316  sumsplitdc  11322  fsum2dlemstep  11324  fisumcom2  11328  fisum0diag2  11337  fsumconst  11344  telfsumo  11356  fsumparts  11360  fsumrelem  11361  binomlem  11373  isumshft  11380  isumsplit  11381  arisum  11388  arisum2  11389  trireciplem  11390  geolim2  11402  geo2sum  11404  0.999...  11411  cvgratz  11422  mertensabs  11427  clim2prod  11429  prodf1f  11433  prodmodclem2a  11466  zproddc  11469  iprodap  11470  iprodap0  11472  fprodseq  11473  prod1dc  11476  prodssdc  11479  fprod2dlemstep  11512  fprodcom2fi  11516  fproddivap  11520  ef0lem  11550  efval2  11555  ege2le3  11561  efaddlem  11564  efsub  11571  eftlub  11580  efsep  11581  tanval3ap  11604  efi4p  11607  sinneg  11616  sinmul  11634  sincossq  11638  cos2t  11640  demoivreALT  11663  eirraplem  11666  dvdsmodexp  11684  odd2np1  11756  omoe  11779  divalglemex  11805  divalglemeuneg  11806  divalgmod  11810  flodddiv4  11817  gcdneg  11857  gcdaddm  11859  modgcd  11866  bezoutlemnewy  11871  gcdass  11890  gcdmultiple  11895  algrp1  11914  lcmneg  11942  lcmgcdeq  11951  lcmass  11953  cncongr2  11972  prmexpb  12016  sqrt2irr  12027  2sqpwodd  12041  qnumdenbi  12057  phiprmpw  12085  eulerthlema  12093  fermltl  12097  prmdiveq  12099  ctiunctlemfo  12151  strslfv3  12206  restuni2  12548  lmfval  12563  cnfval  12565  cnpfval  12566  txtopon  12633  txcnp  12642  upxp  12643  txrest  12647  cnmptcom  12669  bl2in  12774  xblss2  12776  isxms2  12823  setsmsdsg  12851  setsmstsetg  12852  metss  12865  resubmet  12919  cncfcncntop  12951  dvidlemap  13031  dvcnp2cntop  13034  dvcoapbr  13042  dvcjbr  13043  dvexp  13046  dvexp2  13047  dvrecap  13048  efimpi  13111  tangtx  13130  logdivlti  13173  cxpexprp  13187  rpcxpsub  13200  rpabscxpbnd  13230  rprelogbdiv  13245  binom4  13267  bj-charfundcALT  13355  sssneq  13545  0nninf  13547  trilpolemisumle  13580