Theorem eqtr4d 2243

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 2213	. 2 |- ( ph -> B = C )
4	1, 3	eqtrd 2240	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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  3eqtr2d  2246  3eqtr2rd  2247  3eqtr4d  2250  3eqtr4rd  2251  3eqtr4a  2266  sbnfc2  3162  ifsbdc  3592  ifeq1dadc  3610  ifeq2dadc  3611  eqifdc  3616  ifnotdc  3618  2if2dc  3619  ifandc  3620  ifordc  3621  onsucuni2  4630  relop  4846  riinint  4958  iotauni  5263  fniinfv  5660  fsn2  5777  fmptapd  5798  fconst2g  5822  fniunfv  5854  ofres  6196  ofco  6200  caofid1  6210  caofid2  6211  frecsuclem  6515  frecrdg  6517  oasuc  6573  nnacom  6593  nnaass  6594  nndi  6595  nnmass  6596  nnmsucr  6597  nnmcom  6598  funresdfunsndc  6615  uniqs2  6705  en1bg  6915  fundmen  6922  1domsn  6939  pw2f1odclem  6956  mapxpen  6970  xpmapenlem  6971  phplem4dom  6984  en2eqpr  7030  sbthlemi5  7089  omp1eomlem  7222  difinfsnlem  7227  ctmlemr  7236  ctssdccl  7239  ctssdc  7241  infnninf  7252  infnninfOLD  7253  nnnninfeq  7256  pr2cv1  7329  exmidonfinlem  7332  exmidmotap  7408  addcmpblnq  7515  distrnqg  7535  ltexnqq  7556  addcmpblnq0  7591  nqnq0a  7602  nqnq0m  7603  nq0m0r  7604  nq0a0  7605  nnanq0  7606  distrnq0  7607  prarloclemlo  7642  prarloclemcalc  7650  genpassl  7672  genpassu  7673  ltsosr  7912  0idsr  7915  1idsr  7916  mulextsr1lem  7928  cnegex  8285  subsub3  8339  subadd4  8351  mulneg12  8504  mulsub  8508  apreap  8695  cru  8710  recextlem1  8759  cju  9069  ofnegsub  9070  halfaddsub  9306  nn0supp  9382  nneo  9511  zeo2  9514  uzin  9716  xaddcom  10018  xaddass  10026  xleaddadd  10044  iccf1o  10161  fzsuc2  10236  fldiv4lem1div2uz2  10486  flqeqceilz  10500  zmod1congr  10523  modqcyc  10541  modqcyc2  10542  modqaddabs  10544  modqmul1  10559  modqaddmulmod  10573  addmodlteq  10580  frec2uzrdg  10591  frecuzrdgsuctlem  10605  seq3val  10642  seqvalcd  10643  seq3fveq2  10657  seqfveq2g  10659  seq3split  10670  seqsplitg  10671  seqf1oglem2a  10700  seqf1oglem2  10702  seqfeq4g  10713  seq3distr  10714  ser0f  10716  expp1  10728  mulexp  10760  mulexpzap  10761  expadd  10763  expaddzap  10765  expmul  10766  expmulzap  10767  expsubap  10769  expdivap  10772  subsq  10828  mulbinom2  10838  binom3  10839  bernneq  10842  modqexp  10848  nn0opthd  10904  faclbnd  10923  faclbnd6  10926  bccmpl  10936  bcp1n  10943  zfz1isolemiso  11021  seq3coll  11024  ccatsymb  11096  ccatval1lsw  11098  ccatass  11102  eqs1  11120  lswccats1fst  11134  swrdsb0eq  11156  swrdsbslen  11157  swrds1  11159  ccatswrd  11161  pfxres  11172  ccatpfx  11192  pfxpfx  11199  cats1un  11212  swrdccatin1  11216  pfxccatin12  11224  swrdccat  11226  pfxccat3a  11229  swrdccat3b  11231  shftval2  11252  shftval4  11254  seq3shft  11264  crre  11283  remim  11286  remullem  11297  cjexp  11319  cnrecnv  11336  resqrexlemlo  11439  resqrexlemcalc1  11440  resqrexlemcalc2  11441  resqrexlemcalc3  11442  resqrexlemnm  11444  rsqrmo  11453  abscj  11478  absid  11497  absre  11503  recvalap  11523  maxabsle  11630  maxltsup  11644  2zsupmax  11652  minabs  11662  bdtrilem  11665  bdtri  11666  2zinfmin  11669  xrmaxiflemab  11673  xrmaxiflemcom  11675  xrmaxadd  11687  xrbdtri  11702  iooinsup  11703  climaddc1  11755  climmulc2  11757  climsubc1  11758  climsubc2  11759  climcvg1nlem  11775  summodclem3  11806  zsumdc  11810  isum  11811  isumz  11815  isumss  11817  fisumss  11818  fsum3cvg2  11820  fsumadd  11832  isummulc2  11852  sumsplitdc  11858  fsum2dlemstep  11860  fisumcom2  11864  fisum0diag2  11873  fsumconst  11880  telfsumo  11892  fsumparts  11896  fsumrelem  11897  binomlem  11909  isumshft  11916  isumsplit  11917  arisum  11924  arisum2  11925  trireciplem  11926  geolim2  11938  geo2sum  11940  0.999...  11947  cvgratz  11958  mertensabs  11963  clim2prod  11965  prodf1f  11969  prodmodclem2a  12002  zproddc  12005  iprodap  12006  iprodap0  12008  fprodseq  12009  prod1dc  12012  prodssdc  12015  fprod2dlemstep  12048  fprodcom2fi  12052  fproddivap  12056  ef0lem  12086  efval2  12091  ege2le3  12097  efaddlem  12100  efsub  12107  eftlub  12116  efsep  12117  tanval3ap  12140  efi4p  12143  sinneg  12152  sinmul  12170  sincossq  12174  cos2t  12176  demoivreALT  12200  eirraplem  12203  dvdsmodexp  12221  odd2np1  12299  omoe  12322  divalglemex  12348  divalglemeuneg  12349  divalgmod  12353  flodddiv4  12362  bitsp1  12377  bitsinv1lem  12387  bitsinv1  12388  gcdneg  12418  gcdaddm  12420  modgcd  12427  bezoutlemnewy  12432  gcdass  12451  gcdmultiple  12456  nninfctlemfo  12476  algrp1  12483  lcmneg  12511  lcmgcdeq  12520  lcmass  12522  cncongr2  12541  prmexpb  12588  sqrt2irr  12599  2sqpwodd  12613  qnumdenbi  12629  phiprmpw  12659  eulerthlema  12667  fermltl  12671  prmdiveq  12673  modprm0  12692  pythagtriplem1  12703  pythagtriplem12  12713  pythagtriplem14  12715  pythagtriplem15  12716  pythagtriplem16  12717  pythagtriplem17  12718  pythagtriplem19  12720  pcpremul  12731  pcneg  12763  pcgcd  12767  pc2dvds  12768  pcaddlem  12777  pcprod  12784  fldivp1  12786  pcbc  12789  prmpwdvds  12793  pockthlem  12794  mul4sqlem  12831  4sqlem11  12839  4sqlem12  12840  4sqlem17  12845  ctiunctlemfo  12925  ressval3d  13019  resseqnbasd  13020  prdsval  13220  imasival  13253  qusval  13270  plusfeqg  13311  sgrp1  13358  idmhm  13416  resmhm2  13435  mhmeql  13439  grppropstrg  13466  grpinvinv  13514  grp1  13553  imasgrp2  13561  mulgnngsum  13578  mulginvcom  13598  mulgnndir  13602  mulgdir  13605  mulgneg2  13607  mulgnnass  13608  mulgass  13610  mulgsubdir  13613  trivsubgd  13651  nmzsubg  13661  qussub  13688  idghm  13710  ablinvadd  13761  ablsub2inv  13762  eqgabl  13781  mgpplusgg  13801  mgpbasg  13803  mgpscag  13804  mgptsetg  13805  mgpdsg  13807  mgpress  13808  srgpcomp  13867  srgpcompp  13868  ringo2times  13905  ring1eq0  13925  ring1  13936  opprmulfvalg  13947  crngoppr  13949  opprsllem  13951  oppr1g  13959  opprunitd  13987  rdivmuldivd  14021  rhmunitinv  14055  scafeqg  14185  lmodvsubval2  14219  lmodsubdi  14221  rmodislmod  14228  sralemg  14315  sraipg  14321  crng2idl  14408  cnfldmulg  14453  cnfldexp  14454  cnfldui  14466  mulgrhm2  14487  zrhrhmb  14499  zlmvscag  14510  znval2  14515  znbaslemnn  14516  znunit  14536  psrval  14543  psrgrp  14562  psrneg  14564  mplval2g  14572  restuni2  14764  lmfval  14779  cnfval  14781  cnpfval  14782  txtopon  14849  txcnp  14858  upxp  14859  txrest  14863  cnmptcom  14885  bl2in  14990  xblss2  14992  isxms2  15039  setsmsdsg  15067  setsmstsetg  15068  metss  15081  resubmet  15143  expcn  15156  cncfcncntop  15180  dvidlemap  15278  dvidrelem  15279  dvidsslem  15280  dvcnp2cntop  15286  dvcoapbr  15294  dvcjbr  15295  dvexp  15298  dvexp2  15299  dvrecap  15300  plyaddlem1  15334  plymullem1  15335  plycolemc  15345  plycjlemc  15347  dvply1  15352  efimpi  15406  tangtx  15425  logdivlti  15468  cxpexprp  15482  rpcxpsub  15495  rpabscxpbnd  15527  rprelogbdiv  15544  binom4  15566  mpodvdsmulf1o  15577  0sgmppw  15580  lgslem1  15592  lgsmod  15618  lgsdilem  15619  lgsdi  15629  lgsne0  15630  lgsdirnn0  15639  lgsdinn0  15640  lgseisenlem2  15663  lgseisenlem3  15664  lgsquadlem2  15670  lgsquadlem3  15671  lgsquad2lem1  15673  lgsquad3  15676  2lgslem3  15693  2lgsoddprmlem2  15698  2sqlem4  15710  basvtxval2dom  15748  edgfiedgval2dom  15749  bj-charfundcALT  15944  1dom1el  16126  2omap  16132  sssneq  16141  0nninf  16143  nnnninfex  16161  nninfnfiinf  16162  trilpolemisumle  16179