Theorem eqtr4d 2241

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

Syntax hints:   -> wi 4   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  3eqtr2d  2244  3eqtr2rd  2245  3eqtr4d  2248  3eqtr4rd  2249  3eqtr4a  2264  sbnfc2  3154  ifsbdc  3583  ifeq1dadc  3601  ifeq2dadc  3602  eqifdc  3607  ifnotdc  3609  ifandc  3610  ifordc  3611  onsucuni2  4612  relop  4828  riinint  4939  iotauni  5244  fniinfv  5637  fsn2  5754  fmptapd  5775  fconst2g  5799  fniunfv  5831  ofres  6173  ofco  6177  caofid1  6187  caofid2  6188  frecsuclem  6492  frecrdg  6494  oasuc  6550  nnacom  6570  nnaass  6571  nndi  6572  nnmass  6573  nnmsucr  6574  nnmcom  6575  funresdfunsndc  6592  uniqs2  6682  en1bg  6892  fundmen  6898  1domsn  6914  pw2f1odclem  6931  mapxpen  6945  xpmapenlem  6946  phplem4dom  6959  en2eqpr  7004  sbthlemi5  7063  omp1eomlem  7196  difinfsnlem  7201  ctmlemr  7210  ctssdccl  7213  ctssdc  7215  infnninf  7226  infnninfOLD  7227  nnnninfeq  7230  exmidonfinlem  7301  exmidmotap  7373  addcmpblnq  7480  distrnqg  7500  ltexnqq  7521  addcmpblnq0  7556  nqnq0a  7567  nqnq0m  7568  nq0m0r  7569  nq0a0  7570  nnanq0  7571  distrnq0  7572  prarloclemlo  7607  prarloclemcalc  7615  genpassl  7637  genpassu  7638  ltsosr  7877  0idsr  7880  1idsr  7881  mulextsr1lem  7893  cnegex  8250  subsub3  8304  subadd4  8316  mulneg12  8469  mulsub  8473  apreap  8660  cru  8675  recextlem1  8724  cju  9034  ofnegsub  9035  halfaddsub  9271  nn0supp  9347  nneo  9476  zeo2  9479  uzin  9681  xaddcom  9983  xaddass  9991  xleaddadd  10009  iccf1o  10126  fzsuc2  10201  fldiv4lem1div2uz2  10449  flqeqceilz  10463  zmod1congr  10486  modqcyc  10504  modqcyc2  10505  modqaddabs  10507  modqmul1  10522  modqaddmulmod  10536  addmodlteq  10543  frec2uzrdg  10554  frecuzrdgsuctlem  10568  seq3val  10605  seqvalcd  10606  seq3fveq2  10620  seqfveq2g  10622  seq3split  10633  seqsplitg  10634  seqf1oglem2a  10663  seqf1oglem2  10665  seqfeq4g  10676  seq3distr  10677  ser0f  10679  expp1  10691  mulexp  10723  mulexpzap  10724  expadd  10726  expaddzap  10728  expmul  10729  expmulzap  10730  expsubap  10732  expdivap  10735  subsq  10791  mulbinom2  10801  binom3  10802  bernneq  10805  modqexp  10811  nn0opthd  10867  faclbnd  10886  faclbnd6  10889  bccmpl  10899  bcp1n  10906  zfz1isolemiso  10984  seq3coll  10987  ccatsymb  11058  ccatval1lsw  11060  ccatass  11064  eqs1  11082  lswccats1fst  11096  swrdsb0eq  11118  swrdsbslen  11119  swrds1  11121  ccatswrd  11123  shftval2  11137  shftval4  11139  seq3shft  11149  crre  11168  remim  11171  remullem  11182  cjexp  11204  cnrecnv  11221  resqrexlemlo  11324  resqrexlemcalc1  11325  resqrexlemcalc2  11326  resqrexlemcalc3  11327  resqrexlemnm  11329  rsqrmo  11338  abscj  11363  absid  11382  absre  11388  recvalap  11408  maxabsle  11515  maxltsup  11529  2zsupmax  11537  minabs  11547  bdtrilem  11550  bdtri  11551  2zinfmin  11554  xrmaxiflemab  11558  xrmaxiflemcom  11560  xrmaxadd  11572  xrbdtri  11587  iooinsup  11588  climaddc1  11640  climmulc2  11642  climsubc1  11643  climsubc2  11644  climcvg1nlem  11660  summodclem3  11691  zsumdc  11695  isum  11696  isumz  11700  isumss  11702  fisumss  11703  fsum3cvg2  11705  fsumadd  11717  isummulc2  11737  sumsplitdc  11743  fsum2dlemstep  11745  fisumcom2  11749  fisum0diag2  11758  fsumconst  11765  telfsumo  11777  fsumparts  11781  fsumrelem  11782  binomlem  11794  isumshft  11801  isumsplit  11802  arisum  11809  arisum2  11810  trireciplem  11811  geolim2  11823  geo2sum  11825  0.999...  11832  cvgratz  11843  mertensabs  11848  clim2prod  11850  prodf1f  11854  prodmodclem2a  11887  zproddc  11890  iprodap  11891  iprodap0  11893  fprodseq  11894  prod1dc  11897  prodssdc  11900  fprod2dlemstep  11933  fprodcom2fi  11937  fproddivap  11941  ef0lem  11971  efval2  11976  ege2le3  11982  efaddlem  11985  efsub  11992  eftlub  12001  efsep  12002  tanval3ap  12025  efi4p  12028  sinneg  12037  sinmul  12055  sincossq  12059  cos2t  12061  demoivreALT  12085  eirraplem  12088  dvdsmodexp  12106  odd2np1  12184  omoe  12207  divalglemex  12233  divalglemeuneg  12234  divalgmod  12238  flodddiv4  12247  bitsp1  12262  bitsinv1lem  12272  bitsinv1  12273  gcdneg  12303  gcdaddm  12305  modgcd  12312  bezoutlemnewy  12317  gcdass  12336  gcdmultiple  12341  nninfctlemfo  12361  algrp1  12368  lcmneg  12396  lcmgcdeq  12405  lcmass  12407  cncongr2  12426  prmexpb  12473  sqrt2irr  12484  2sqpwodd  12498  qnumdenbi  12514  phiprmpw  12544  eulerthlema  12552  fermltl  12556  prmdiveq  12558  modprm0  12577  pythagtriplem1  12588  pythagtriplem12  12598  pythagtriplem14  12600  pythagtriplem15  12601  pythagtriplem16  12602  pythagtriplem17  12603  pythagtriplem19  12605  pcpremul  12616  pcneg  12648  pcgcd  12652  pc2dvds  12653  pcaddlem  12662  pcprod  12669  fldivp1  12671  pcbc  12674  prmpwdvds  12678  pockthlem  12679  mul4sqlem  12716  4sqlem11  12724  4sqlem12  12725  4sqlem17  12730  ctiunctlemfo  12810  ressval3d  12904  resseqnbasd  12905  prdsval  13105  imasival  13138  qusval  13155  plusfeqg  13196  sgrp1  13243  idmhm  13301  resmhm2  13320  mhmeql  13324  grppropstrg  13351  grpinvinv  13399  grp1  13438  imasgrp2  13446  mulgnngsum  13463  mulginvcom  13483  mulgnndir  13487  mulgdir  13490  mulgneg2  13492  mulgnnass  13493  mulgass  13495  mulgsubdir  13498  trivsubgd  13536  nmzsubg  13546  qussub  13573  idghm  13595  ablinvadd  13646  ablsub2inv  13647  eqgabl  13666  mgpplusgg  13686  mgpbasg  13688  mgpscag  13689  mgptsetg  13690  mgpdsg  13692  mgpress  13693  srgpcomp  13752  srgpcompp  13753  ringo2times  13790  ring1eq0  13810  ring1  13821  opprmulfvalg  13832  crngoppr  13834  opprsllem  13836  oppr1g  13844  opprunitd  13872  rdivmuldivd  13906  rhmunitinv  13940  scafeqg  14070  lmodvsubval2  14104  lmodsubdi  14106  rmodislmod  14113  sralemg  14200  sraipg  14206  crng2idl  14293  cnfldmulg  14338  cnfldexp  14339  cnfldui  14351  mulgrhm2  14372  zrhrhmb  14384  zlmvscag  14395  znval2  14400  znbaslemnn  14401  znunit  14421  psrval  14428  psrgrp  14447  psrneg  14449  mplval2g  14457  restuni2  14649  lmfval  14664  cnfval  14666  cnpfval  14667  txtopon  14734  txcnp  14743  upxp  14744  txrest  14748  cnmptcom  14770  bl2in  14875  xblss2  14877  isxms2  14924  setsmsdsg  14952  setsmstsetg  14953  metss  14966  resubmet  15028  expcn  15041  cncfcncntop  15065  dvidlemap  15163  dvidrelem  15164  dvidsslem  15165  dvcnp2cntop  15171  dvcoapbr  15179  dvcjbr  15180  dvexp  15183  dvexp2  15184  dvrecap  15185  plyaddlem1  15219  plymullem1  15220  plycolemc  15230  plycjlemc  15232  dvply1  15237  efimpi  15291  tangtx  15310  logdivlti  15353  cxpexprp  15367  rpcxpsub  15380  rpabscxpbnd  15412  rprelogbdiv  15429  binom4  15451  mpodvdsmulf1o  15462  0sgmppw  15465  lgslem1  15477  lgsmod  15503  lgsdilem  15504  lgsdi  15514  lgsne0  15515  lgsdirnn0  15524  lgsdinn0  15525  lgseisenlem2  15548  lgseisenlem3  15549  lgsquadlem2  15555  lgsquadlem3  15556  lgsquad2lem1  15558  lgsquad3  15561  2lgslem3  15578  2lgsoddprmlem2  15583  2sqlem4  15595  basvtxval2dom  15631  edgfiedgval2dom  15632  bj-charfundcALT  15745  1dom1el  15927  2omap  15932  sssneq  15939  0nninf  15941  nnnninfex  15959  nninfnfiinf  15960  trilpolemisumle  15977