Theorem eqtr4d 2176

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

Syntax hints:   -> wi 4   = wceq 1332

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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

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

This theorem is referenced by:  3eqtr2d  2179  3eqtr2rd  2180  3eqtr4d  2183  3eqtr4rd  2184  3eqtr4a  2199  sbnfc2  3065  ifsbdc  3491  ifeq1dadc  3507  eqifdc  3511  ifandc  3513  onsucuni2  4487  relop  4697  riinint  4808  iotauni  5108  fniinfv  5487  fsn2  5602  fmptapd  5619  fconst2g  5643  fniunfv  5671  ofres  6004  ofco  6008  frecsuclem  6311  frecrdg  6313  oasuc  6368  nnacom  6388  nnaass  6389  nndi  6390  nnmass  6391  nnmsucr  6392  nnmcom  6393  funresdfunsndc  6410  uniqs2  6497  en1bg  6702  fundmen  6708  1domsn  6721  mapxpen  6750  xpmapenlem  6751  phplem4dom  6764  en2eqpr  6809  sbthlemi5  6857  omp1eomlem  6987  difinfsnlem  6992  ctmlemr  7001  ctssdccl  7004  ctssdc  7006  infnninf  7030  exmidonfinlem  7066  addcmpblnq  7199  distrnqg  7219  ltexnqq  7240  addcmpblnq0  7275  nqnq0a  7286  nqnq0m  7287  nq0m0r  7288  nq0a0  7289  nnanq0  7290  distrnq0  7291  prarloclemlo  7326  prarloclemcalc  7334  genpassl  7356  genpassu  7357  ltsosr  7596  0idsr  7599  1idsr  7600  mulextsr1lem  7612  cnegex  7964  subsub3  8018  subadd4  8030  mulneg12  8183  mulsub  8187  apreap  8373  cru  8388  recextlem1  8436  cju  8743  halfaddsub  8978  nn0supp  9053  nneo  9178  zeo2  9181  uzin  9382  xaddcom  9674  xaddass  9682  xleaddadd  9700  iccf1o  9817  fzsuc2  9890  flqeqceilz  10122  zmod1congr  10145  modqcyc  10163  modqcyc2  10164  modqaddabs  10166  modqmul1  10181  modqaddmulmod  10195  addmodlteq  10202  frec2uzrdg  10213  frecuzrdgsuctlem  10227  seq3val  10262  seqvalcd  10263  seq3fveq2  10273  seq3split  10283  seq3distr  10317  ser0f  10319  expp1  10331  mulexp  10363  mulexpzap  10364  expadd  10366  expaddzap  10368  expmul  10369  expmulzap  10370  expsubap  10372  expdivap  10375  subsq  10430  mulbinom2  10439  binom3  10440  bernneq  10443  nn0opthd  10500  faclbnd  10519  faclbnd6  10522  bccmpl  10532  bcp1n  10539  zfz1isolemiso  10614  seq3coll  10617  shftval2  10630  shftval4  10632  seq3shft  10642  crre  10661  remim  10664  remullem  10675  cjexp  10697  cnrecnv  10714  resqrexlemlo  10817  resqrexlemcalc1  10818  resqrexlemcalc2  10819  resqrexlemcalc3  10820  resqrexlemnm  10822  rsqrmo  10831  abscj  10856  absid  10875  absre  10881  recvalap  10901  maxabsle  11008  maxltsup  11022  2zsupmax  11029  minabs  11039  bdtrilem  11042  bdtri  11043  xrmaxiflemab  11048  xrmaxiflemcom  11050  xrmaxadd  11062  xrbdtri  11077  iooinsup  11078  climaddc1  11130  climmulc2  11132  climsubc1  11133  climsubc2  11134  climcvg1nlem  11150  summodclem3  11181  zsumdc  11185  isum  11186  isumz  11190  isumss  11192  fisumss  11193  fsum3cvg2  11195  fsumadd  11207  isummulc2  11227  sumsplitdc  11233  fsum2dlemstep  11235  fisumcom2  11239  fisum0diag2  11248  fsumconst  11255  telfsumo  11267  fsumparts  11271  fsumrelem  11272  binomlem  11284  isumshft  11291  isumsplit  11292  arisum  11299  arisum2  11300  trireciplem  11301  geolim2  11313  geo2sum  11315  0.999...  11322  cvgratz  11333  mertensabs  11338  clim2prod  11340  prodf1f  11344  prodmodclem2a  11377  zproddc  11380  iprodap  11381  iprodap0  11383  fprodseq  11384  ef0lem  11403  efval2  11408  ege2le3  11414  efaddlem  11417  efsub  11424  eftlub  11433  efsep  11434  tanval3ap  11457  efi4p  11460  sinneg  11469  sinmul  11487  sincossq  11491  cos2t  11493  demoivreALT  11516  eirraplem  11519  odd2np1  11606  omoe  11629  divalglemex  11655  divalglemeuneg  11656  divalgmod  11660  flodddiv4  11667  gcdneg  11706  gcdaddm  11708  modgcd  11715  bezoutlemnewy  11720  gcdass  11739  gcdmultiple  11744  algrp1  11763  lcmneg  11791  lcmgcdeq  11800  lcmass  11802  cncongr2  11821  prmexpb  11865  sqrt2irr  11876  2sqpwodd  11890  qnumdenbi  11906  phiprmpw  11934  ctiunctlemfo  11988  strslfv3  12043  restuni2  12385  lmfval  12400  cnfval  12402  cnpfval  12403  txtopon  12470  txcnp  12479  upxp  12480  txrest  12484  cnmptcom  12506  bl2in  12611  xblss2  12613  isxms2  12660  setsmsdsg  12688  setsmstsetg  12689  metss  12702  resubmet  12756  cncfcncntop  12788  dvidlemap  12868  dvcnp2cntop  12871  dvcoapbr  12879  dvcjbr  12880  dvexp  12883  dvexp2  12884  dvrecap  12885  efimpi  12948  tangtx  12967  logdivlti  13010  cxpexprp  13024  rpcxpsub  13037  rpabscxpbnd  13067  rprelogbdiv  13082  sssneq  13370  0nninf  13372  nninfalllemn  13377  trilpolemisumle  13406