Theorem eqtr4d 2232

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

Syntax hints:   -> wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  3eqtr2d  2235  3eqtr2rd  2236  3eqtr4d  2239  3eqtr4rd  2240  3eqtr4a  2255  sbnfc2  3145  ifsbdc  3574  ifeq1dadc  3592  ifeq2dadc  3593  eqifdc  3597  ifnotdc  3599  ifandc  3600  ifordc  3601  onsucuni2  4601  relop  4817  riinint  4928  iotauni  5232  fniinfv  5622  fsn2  5739  fmptapd  5756  fconst2g  5780  fniunfv  5812  ofres  6154  ofco  6158  caofid1  6168  caofid2  6169  frecsuclem  6473  frecrdg  6475  oasuc  6531  nnacom  6551  nnaass  6552  nndi  6553  nnmass  6554  nnmsucr  6555  nnmcom  6556  funresdfunsndc  6573  uniqs2  6663  en1bg  6868  fundmen  6874  1domsn  6887  pw2f1odclem  6904  mapxpen  6918  xpmapenlem  6919  phplem4dom  6932  en2eqpr  6977  sbthlemi5  7036  omp1eomlem  7169  difinfsnlem  7174  ctmlemr  7183  ctssdccl  7186  ctssdc  7188  infnninf  7199  infnninfOLD  7200  nnnninfeq  7203  exmidonfinlem  7272  exmidmotap  7344  addcmpblnq  7451  distrnqg  7471  ltexnqq  7492  addcmpblnq0  7527  nqnq0a  7538  nqnq0m  7539  nq0m0r  7540  nq0a0  7541  nnanq0  7542  distrnq0  7543  prarloclemlo  7578  prarloclemcalc  7586  genpassl  7608  genpassu  7609  ltsosr  7848  0idsr  7851  1idsr  7852  mulextsr1lem  7864  cnegex  8221  subsub3  8275  subadd4  8287  mulneg12  8440  mulsub  8444  apreap  8631  cru  8646  recextlem1  8695  cju  9005  ofnegsub  9006  halfaddsub  9242  nn0supp  9318  nneo  9446  zeo2  9449  uzin  9651  xaddcom  9953  xaddass  9961  xleaddadd  9979  iccf1o  10096  fzsuc2  10171  fldiv4lem1div2uz2  10413  flqeqceilz  10427  zmod1congr  10450  modqcyc  10468  modqcyc2  10469  modqaddabs  10471  modqmul1  10486  modqaddmulmod  10500  addmodlteq  10507  frec2uzrdg  10518  frecuzrdgsuctlem  10532  seq3val  10569  seqvalcd  10570  seq3fveq2  10584  seqfveq2g  10586  seq3split  10597  seqsplitg  10598  seqf1oglem2a  10627  seqf1oglem2  10629  seqfeq4g  10640  seq3distr  10641  ser0f  10643  expp1  10655  mulexp  10687  mulexpzap  10688  expadd  10690  expaddzap  10692  expmul  10693  expmulzap  10694  expsubap  10696  expdivap  10699  subsq  10755  mulbinom2  10765  binom3  10766  bernneq  10769  modqexp  10775  nn0opthd  10831  faclbnd  10850  faclbnd6  10853  bccmpl  10863  bcp1n  10870  zfz1isolemiso  10948  seq3coll  10951  shftval2  11008  shftval4  11010  seq3shft  11020  crre  11039  remim  11042  remullem  11053  cjexp  11075  cnrecnv  11092  resqrexlemlo  11195  resqrexlemcalc1  11196  resqrexlemcalc2  11197  resqrexlemcalc3  11198  resqrexlemnm  11200  rsqrmo  11209  abscj  11234  absid  11253  absre  11259  recvalap  11279  maxabsle  11386  maxltsup  11400  2zsupmax  11408  minabs  11418  bdtrilem  11421  bdtri  11422  2zinfmin  11425  xrmaxiflemab  11429  xrmaxiflemcom  11431  xrmaxadd  11443  xrbdtri  11458  iooinsup  11459  climaddc1  11511  climmulc2  11513  climsubc1  11514  climsubc2  11515  climcvg1nlem  11531  summodclem3  11562  zsumdc  11566  isum  11567  isumz  11571  isumss  11573  fisumss  11574  fsum3cvg2  11576  fsumadd  11588  isummulc2  11608  sumsplitdc  11614  fsum2dlemstep  11616  fisumcom2  11620  fisum0diag2  11629  fsumconst  11636  telfsumo  11648  fsumparts  11652  fsumrelem  11653  binomlem  11665  isumshft  11672  isumsplit  11673  arisum  11680  arisum2  11681  trireciplem  11682  geolim2  11694  geo2sum  11696  0.999...  11703  cvgratz  11714  mertensabs  11719  clim2prod  11721  prodf1f  11725  prodmodclem2a  11758  zproddc  11761  iprodap  11762  iprodap0  11764  fprodseq  11765  prod1dc  11768  prodssdc  11771  fprod2dlemstep  11804  fprodcom2fi  11808  fproddivap  11812  ef0lem  11842  efval2  11847  ege2le3  11853  efaddlem  11856  efsub  11863  eftlub  11872  efsep  11873  tanval3ap  11896  efi4p  11899  sinneg  11908  sinmul  11926  sincossq  11930  cos2t  11932  demoivreALT  11956  eirraplem  11959  dvdsmodexp  11977  odd2np1  12055  omoe  12078  divalglemex  12104  divalglemeuneg  12105  divalgmod  12109  flodddiv4  12118  bitsp1  12133  bitsinv1lem  12143  bitsinv1  12144  gcdneg  12174  gcdaddm  12176  modgcd  12183  bezoutlemnewy  12188  gcdass  12207  gcdmultiple  12212  nninfctlemfo  12232  algrp1  12239  lcmneg  12267  lcmgcdeq  12276  lcmass  12278  cncongr2  12297  prmexpb  12344  sqrt2irr  12355  2sqpwodd  12369  qnumdenbi  12385  phiprmpw  12415  eulerthlema  12423  fermltl  12427  prmdiveq  12429  modprm0  12448  pythagtriplem1  12459  pythagtriplem12  12469  pythagtriplem14  12471  pythagtriplem15  12472  pythagtriplem16  12473  pythagtriplem17  12474  pythagtriplem19  12476  pcpremul  12487  pcneg  12519  pcgcd  12523  pc2dvds  12524  pcaddlem  12533  pcprod  12540  fldivp1  12542  pcbc  12545  prmpwdvds  12549  pockthlem  12550  mul4sqlem  12587  4sqlem11  12595  4sqlem12  12596  4sqlem17  12601  ctiunctlemfo  12681  ressval3d  12775  resseqnbasd  12776  prdsval  12975  imasival  13008  qusval  13025  plusfeqg  13066  sgrp1  13113  idmhm  13171  resmhm2  13190  mhmeql  13194  grppropstrg  13221  grpinvinv  13269  grp1  13308  imasgrp2  13316  mulgnngsum  13333  mulginvcom  13353  mulgnndir  13357  mulgdir  13360  mulgneg2  13362  mulgnnass  13363  mulgass  13365  mulgsubdir  13368  trivsubgd  13406  nmzsubg  13416  qussub  13443  idghm  13465  ablinvadd  13516  ablsub2inv  13517  eqgabl  13536  mgpplusgg  13556  mgpbasg  13558  mgpscag  13559  mgptsetg  13560  mgpdsg  13562  mgpress  13563  srgpcomp  13622  srgpcompp  13623  ringo2times  13660  ring1eq0  13680  ring1  13691  opprmulfvalg  13702  crngoppr  13704  opprsllem  13706  oppr1g  13714  opprunitd  13742  rdivmuldivd  13776  rhmunitinv  13810  scafeqg  13940  lmodvsubval2  13974  lmodsubdi  13976  rmodislmod  13983  sralemg  14070  sraipg  14076  crng2idl  14163  cnfldmulg  14208  cnfldexp  14209  cnfldui  14221  mulgrhm2  14242  zrhrhmb  14254  zlmvscag  14265  znval2  14270  znbaslemnn  14271  znunit  14291  psrval  14296  psrgrp  14313  psrneg  14315  restuni2  14497  lmfval  14512  cnfval  14514  cnpfval  14515  txtopon  14582  txcnp  14591  upxp  14592  txrest  14596  cnmptcom  14618  bl2in  14723  xblss2  14725  isxms2  14772  setsmsdsg  14800  setsmstsetg  14801  metss  14814  resubmet  14876  expcn  14889  cncfcncntop  14913  dvidlemap  15011  dvidrelem  15012  dvidsslem  15013  dvcnp2cntop  15019  dvcoapbr  15027  dvcjbr  15028  dvexp  15031  dvexp2  15032  dvrecap  15033  plyaddlem1  15067  plymullem1  15068  plycolemc  15078  plycjlemc  15080  dvply1  15085  efimpi  15139  tangtx  15158  logdivlti  15201  cxpexprp  15215  rpcxpsub  15228  rpabscxpbnd  15260  rprelogbdiv  15277  binom4  15299  mpodvdsmulf1o  15310  0sgmppw  15313  lgslem1  15325  lgsmod  15351  lgsdilem  15352  lgsdi  15362  lgsne0  15363  lgsdirnn0  15372  lgsdinn0  15373  lgseisenlem2  15396  lgseisenlem3  15397  lgsquadlem2  15403  lgsquadlem3  15404  lgsquad2lem1  15406  lgsquad3  15409  2lgslem3  15426  2lgsoddprmlem2  15431  2sqlem4  15443  bj-charfundcALT  15539  1dom1el  15721  2omap  15726  sssneq  15733  0nninf  15735  trilpolemisumle  15769