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  4562  relop  4776  riinint  4887  iotauni  5189  fniinfv  5573  fsn2  5689  fmptapd  5706  fconst2g  5730  fniunfv  5760  ofres  6094  ofco  6098  frecsuclem  6404  frecrdg  6406  oasuc  6462  nnacom  6482  nnaass  6483  nndi  6484  nnmass  6485  nnmsucr  6486  nnmcom  6487  funresdfunsndc  6504  uniqs2  6592  en1bg  6797  fundmen  6803  1domsn  6816  mapxpen  6845  xpmapenlem  6846  phplem4dom  6859  en2eqpr  6904  sbthlemi5  6957  omp1eomlem  7090  difinfsnlem  7095  ctmlemr  7104  ctssdccl  7107  ctssdc  7109  infnninf  7119  infnninfOLD  7120  nnnninfeq  7123  exmidonfinlem  7189  exmidmotap  7257  addcmpblnq  7363  distrnqg  7383  ltexnqq  7404  addcmpblnq0  7439  nqnq0a  7450  nqnq0m  7451  nq0m0r  7452  nq0a0  7453  nnanq0  7454  distrnq0  7455  prarloclemlo  7490  prarloclemcalc  7498  genpassl  7520  genpassu  7521  ltsosr  7760  0idsr  7763  1idsr  7764  mulextsr1lem  7776  cnegex  8131  subsub3  8185  subadd4  8197  mulneg12  8350  mulsub  8354  apreap  8540  cru  8555  recextlem1  8604  cju  8914  halfaddsub  9149  nn0supp  9224  nneo  9352  zeo2  9355  uzin  9556  xaddcom  9857  xaddass  9865  xleaddadd  9883  iccf1o  10000  fzsuc2  10074  flqeqceilz  10313  zmod1congr  10336  modqcyc  10354  modqcyc2  10355  modqaddabs  10357  modqmul1  10372  modqaddmulmod  10386  addmodlteq  10393  frec2uzrdg  10404  frecuzrdgsuctlem  10418  seq3val  10453  seqvalcd  10454  seq3fveq2  10464  seq3split  10474  seq3distr  10508  ser0f  10510  expp1  10522  mulexp  10554  mulexpzap  10555  expadd  10557  expaddzap  10559  expmul  10560  expmulzap  10561  expsubap  10563  expdivap  10566  subsq  10621  mulbinom2  10631  binom3  10632  bernneq  10635  modqexp  10641  nn0opthd  10695  faclbnd  10714  faclbnd6  10717  bccmpl  10727  bcp1n  10734  zfz1isolemiso  10812  seq3coll  10815  shftval2  10828  shftval4  10830  seq3shft  10840  crre  10859  remim  10862  remullem  10873  cjexp  10895  cnrecnv  10912  resqrexlemlo  11015  resqrexlemcalc1  11016  resqrexlemcalc2  11017  resqrexlemcalc3  11018  resqrexlemnm  11020  rsqrmo  11029  abscj  11054  absid  11073  absre  11079  recvalap  11099  maxabsle  11206  maxltsup  11220  2zsupmax  11227  minabs  11237  bdtrilem  11240  bdtri  11241  2zinfmin  11244  xrmaxiflemab  11248  xrmaxiflemcom  11250  xrmaxadd  11262  xrbdtri  11277  iooinsup  11278  climaddc1  11330  climmulc2  11332  climsubc1  11333  climsubc2  11334  climcvg1nlem  11350  summodclem3  11381  zsumdc  11385  isum  11386  isumz  11390  isumss  11392  fisumss  11393  fsum3cvg2  11395  fsumadd  11407  isummulc2  11427  sumsplitdc  11433  fsum2dlemstep  11435  fisumcom2  11439  fisum0diag2  11448  fsumconst  11455  telfsumo  11467  fsumparts  11471  fsumrelem  11472  binomlem  11484  isumshft  11491  isumsplit  11492  arisum  11499  arisum2  11500  trireciplem  11501  geolim2  11513  geo2sum  11515  0.999...  11522  cvgratz  11533  mertensabs  11538  clim2prod  11540  prodf1f  11544  prodmodclem2a  11577  zproddc  11580  iprodap  11581  iprodap0  11583  fprodseq  11584  prod1dc  11587  prodssdc  11590  fprod2dlemstep  11623  fprodcom2fi  11627  fproddivap  11631  ef0lem  11661  efval2  11666  ege2le3  11672  efaddlem  11675  efsub  11682  eftlub  11691  efsep  11692  tanval3ap  11715  efi4p  11718  sinneg  11727  sinmul  11745  sincossq  11749  cos2t  11751  demoivreALT  11774  eirraplem  11777  dvdsmodexp  11795  odd2np1  11870  omoe  11893  divalglemex  11919  divalglemeuneg  11920  divalgmod  11924  flodddiv4  11931  gcdneg  11975  gcdaddm  11977  modgcd  11984  bezoutlemnewy  11989  gcdass  12008  gcdmultiple  12013  algrp1  12038  lcmneg  12066  lcmgcdeq  12075  lcmass  12077  cncongr2  12096  prmexpb  12143  sqrt2irr  12154  2sqpwodd  12168  qnumdenbi  12184  phiprmpw  12214  eulerthlema  12222  fermltl  12226  prmdiveq  12228  modprm0  12246  pythagtriplem1  12257  pythagtriplem12  12267  pythagtriplem14  12269  pythagtriplem15  12270  pythagtriplem16  12271  pythagtriplem17  12272  pythagtriplem19  12274  pcpremul  12285  pcneg  12316  pcgcd  12320  pc2dvds  12321  pcaddlem  12330  pcprod  12336  fldivp1  12338  pcbc  12341  prmpwdvds  12345  pockthlem  12346  mul4sqlem  12383  ctiunctlemfo  12432  strslfv3  12500  ressval3d  12523  resseqnbasd  12524  plusfeqg  12715  sgrp1  12748  idmhm  12792  mhmeql  12808  grppropstrg  12827  grpinvinv  12869  grp1  12908  mulginvcom  12939  mulgnndir  12943  mulgdir  12946  mulgneg2  12948  mulgnnass  12949  mulgass  12951  mulgsubdir  12954  trivsubgd  12991  nmzsubg  13001  ablinvadd  13044  ablsub2inv  13045  mgpplusgg  13065  mgpbasg  13067  mgpscag  13068  mgptsetg  13069  mgpdsg  13071  mgpress  13072  srgpcomp  13104  srgpcompp  13105  rngo2times  13142  ring1eq0  13156  ring1  13167  opprmulfvalg  13173  crngoppr  13175  opprsllem  13177  oppr1g  13183  opprunitd  13210  rdivmuldivd  13244  cnfldmulg  13339  cnfldexp  13340  restuni2  13548  lmfval  13563  cnfval  13565  cnpfval  13566  txtopon  13633  txcnp  13642  upxp  13643  txrest  13647  cnmptcom  13669  bl2in  13774  xblss2  13776  isxms2  13823  setsmsdsg  13851  setsmstsetg  13852  metss  13865  resubmet  13919  cncfcncntop  13951  dvidlemap  14031  dvcnp2cntop  14034  dvcoapbr  14042  dvcjbr  14043  dvexp  14046  dvexp2  14047  dvrecap  14048  efimpi  14111  tangtx  14130  logdivlti  14173  cxpexprp  14187  rpcxpsub  14200  rpabscxpbnd  14230  rprelogbdiv  14246  binom4  14268  lgslem1  14272  lgsmod  14298  lgsdilem  14299  lgsdi  14309  lgsne0  14310  lgsdirnn0  14319  lgsdinn0  14320  2sqlem4  14325  bj-charfundcALT  14421  sssneq  14611  0nninf  14613  trilpolemisumle  14646