Theorem eqtr4d 2265

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

Syntax hints:   -> wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  3eqtr2d  2268  3eqtr2rd  2269  3eqtr4d  2272  3eqtr4rd  2273  3eqtr4a  2288  sbnfc2  3185  ifsbdc  3615  ifeq1dadc  3633  ifeq2dadc  3634  eqifdc  3639  ifnotdc  3641  2if2dc  3642  ifandc  3643  ifordc  3644  onsucuni2  4656  relop  4872  riinint  4985  iotauni  5291  fniinfv  5694  fsn2  5811  fmptapd  5834  fconst2g  5858  fniunfv  5892  ofres  6239  ofco  6243  caofid1  6253  caofid2  6254  frecsuclem  6558  frecrdg  6560  oasuc  6618  nnacom  6638  nnaass  6639  nndi  6640  nnmass  6641  nnmsucr  6642  nnmcom  6643  funresdfunsndc  6660  uniqs2  6750  en1bg  6960  fundmen  6967  1domsn  6984  pw2f1odclem  7003  mapxpen  7017  xpmapenlem  7018  phplem4dom  7031  en2eqpr  7080  sbthlemi5  7139  omp1eomlem  7272  difinfsnlem  7277  ctmlemr  7286  ctssdccl  7289  ctssdc  7291  infnninf  7302  infnninfOLD  7303  nnnninfeq  7306  pr2cv1  7379  exmidonfinlem  7382  exmidmotap  7458  addcmpblnq  7565  distrnqg  7585  ltexnqq  7606  addcmpblnq0  7641  nqnq0a  7652  nqnq0m  7653  nq0m0r  7654  nq0a0  7655  nnanq0  7656  distrnq0  7657  prarloclemlo  7692  prarloclemcalc  7700  genpassl  7722  genpassu  7723  ltsosr  7962  0idsr  7965  1idsr  7966  mulextsr1lem  7978  cnegex  8335  subsub3  8389  subadd4  8401  mulneg12  8554  mulsub  8558  apreap  8745  cru  8760  recextlem1  8809  cju  9119  ofnegsub  9120  halfaddsub  9356  nn0supp  9432  nneo  9561  zeo2  9564  uzin  9767  xaddcom  10069  xaddass  10077  xleaddadd  10095  iccf1o  10212  fzsuc2  10287  fldiv4lem1div2uz2  10538  flqeqceilz  10552  zmod1congr  10575  modqcyc  10593  modqcyc2  10594  modqaddabs  10596  modqmul1  10611  modqaddmulmod  10625  addmodlteq  10632  frec2uzrdg  10643  frecuzrdgsuctlem  10657  seq3val  10694  seqvalcd  10695  seq3fveq2  10709  seqfveq2g  10711  seq3split  10722  seqsplitg  10723  seqf1oglem2a  10752  seqf1oglem2  10754  seqfeq4g  10765  seq3distr  10766  ser0f  10768  expp1  10780  mulexp  10812  mulexpzap  10813  expadd  10815  expaddzap  10817  expmul  10818  expmulzap  10819  expsubap  10821  expdivap  10824  subsq  10880  mulbinom2  10890  binom3  10891  bernneq  10894  modqexp  10900  nn0opthd  10956  faclbnd  10975  faclbnd6  10978  bccmpl  10988  bcp1n  10995  zfz1isolemiso  11074  seq3coll  11077  ccatsymb  11150  ccatval1lsw  11152  ccatass  11156  eqs1  11176  lswccats1fst  11191  swrdsb0eq  11213  swrdsbslen  11214  swrds1  11216  ccatswrd  11218  pfxres  11229  ccatpfx  11249  pfxpfx  11256  cats1un  11269  swrdccatin1  11273  pfxccatin12  11281  swrdccat  11283  pfxccat3a  11286  swrdccat3b  11288  shftval2  11353  shftval4  11355  seq3shft  11365  crre  11384  remim  11387  remullem  11398  cjexp  11420  cnrecnv  11437  resqrexlemlo  11540  resqrexlemcalc1  11541  resqrexlemcalc2  11542  resqrexlemcalc3  11543  resqrexlemnm  11545  rsqrmo  11554  abscj  11579  absid  11598  absre  11604  recvalap  11624  maxabsle  11731  maxltsup  11745  2zsupmax  11753  minabs  11763  bdtrilem  11766  bdtri  11767  2zinfmin  11770  xrmaxiflemab  11774  xrmaxiflemcom  11776  xrmaxadd  11788  xrbdtri  11803  iooinsup  11804  climaddc1  11856  climmulc2  11858  climsubc1  11859  climsubc2  11860  climcvg1nlem  11876  summodclem3  11907  zsumdc  11911  isum  11912  isumz  11916  isumss  11918  fisumss  11919  fsum3cvg2  11921  fsumadd  11933  isummulc2  11953  sumsplitdc  11959  fsum2dlemstep  11961  fisumcom2  11965  fisum0diag2  11974  fsumconst  11981  telfsumo  11993  fsumparts  11997  fsumrelem  11998  binomlem  12010  isumshft  12017  isumsplit  12018  arisum  12025  arisum2  12026  trireciplem  12027  geolim2  12039  geo2sum  12041  0.999...  12048  cvgratz  12059  mertensabs  12064  clim2prod  12066  prodf1f  12070  prodmodclem2a  12103  zproddc  12106  iprodap  12107  iprodap0  12109  fprodseq  12110  prod1dc  12113  prodssdc  12116  fprod2dlemstep  12149  fprodcom2fi  12153  fproddivap  12157  ef0lem  12187  efval2  12192  ege2le3  12198  efaddlem  12201  efsub  12208  eftlub  12217  efsep  12218  tanval3ap  12241  efi4p  12244  sinneg  12253  sinmul  12271  sincossq  12275  cos2t  12277  demoivreALT  12301  eirraplem  12304  dvdsmodexp  12322  odd2np1  12400  omoe  12423  divalglemex  12449  divalglemeuneg  12450  divalgmod  12454  flodddiv4  12463  bitsp1  12478  bitsinv1lem  12488  bitsinv1  12489  gcdneg  12519  gcdaddm  12521  modgcd  12528  bezoutlemnewy  12533  gcdass  12552  gcdmultiple  12557  nninfctlemfo  12577  algrp1  12584  lcmneg  12612  lcmgcdeq  12621  lcmass  12623  cncongr2  12642  prmexpb  12689  sqrt2irr  12700  2sqpwodd  12714  qnumdenbi  12730  phiprmpw  12760  eulerthlema  12768  fermltl  12772  prmdiveq  12774  modprm0  12793  pythagtriplem1  12804  pythagtriplem12  12814  pythagtriplem14  12816  pythagtriplem15  12817  pythagtriplem16  12818  pythagtriplem17  12819  pythagtriplem19  12821  pcpremul  12832  pcneg  12864  pcgcd  12868  pc2dvds  12869  pcaddlem  12878  pcprod  12885  fldivp1  12887  pcbc  12890  prmpwdvds  12894  pockthlem  12895  mul4sqlem  12932  4sqlem11  12940  4sqlem12  12941  4sqlem17  12946  ctiunctlemfo  13026  ressval3d  13121  resseqnbasd  13122  prdsval  13322  imasival  13355  qusval  13372  plusfeqg  13413  sgrp1  13460  idmhm  13518  resmhm2  13537  mhmeql  13541  grppropstrg  13568  grpinvinv  13616  grp1  13655  imasgrp2  13663  mulgnngsum  13680  mulginvcom  13700  mulgnndir  13704  mulgdir  13707  mulgneg2  13709  mulgnnass  13710  mulgass  13712  mulgsubdir  13715  trivsubgd  13753  nmzsubg  13763  qussub  13790  idghm  13812  ablinvadd  13863  ablsub2inv  13864  eqgabl  13883  mgpplusgg  13903  mgpbasg  13905  mgpscag  13906  mgptsetg  13907  mgpdsg  13909  mgpress  13910  srgpcomp  13969  srgpcompp  13970  ringo2times  14007  ring1eq0  14027  ring1  14038  opprmulfvalg  14049  crngoppr  14051  opprsllem  14053  oppr1g  14061  opprunitd  14090  rdivmuldivd  14124  rhmunitinv  14158  scafeqg  14288  lmodvsubval2  14322  lmodsubdi  14324  rmodislmod  14331  sralemg  14418  sraipg  14424  crng2idl  14511  cnfldmulg  14556  cnfldexp  14557  cnfldui  14569  mulgrhm2  14590  zrhrhmb  14602  zlmvscag  14613  znval2  14618  znbaslemnn  14619  znunit  14639  psrval  14646  psrgrp  14665  psrneg  14667  mplval2g  14675  restuni2  14867  lmfval  14883  cnfval  14884  cnpfval  14885  txtopon  14952  txcnp  14961  upxp  14962  txrest  14966  cnmptcom  14988  bl2in  15093  xblss2  15095  isxms2  15142  setsmsdsg  15170  setsmstsetg  15171  metss  15184  resubmet  15246  expcn  15259  cncfcncntop  15283  dvidlemap  15381  dvidrelem  15382  dvidsslem  15383  dvcnp2cntop  15389  dvcoapbr  15397  dvcjbr  15398  dvexp  15401  dvexp2  15402  dvrecap  15403  plyaddlem1  15437  plymullem1  15438  plycolemc  15448  plycjlemc  15450  dvply1  15455  efimpi  15509  tangtx  15528  logdivlti  15571  cxpexprp  15585  rpcxpsub  15598  rpabscxpbnd  15630  rprelogbdiv  15647  binom4  15669  mpodvdsmulf1o  15680  0sgmppw  15683  lgslem1  15695  lgsmod  15721  lgsdilem  15722  lgsdi  15732  lgsne0  15733  lgsdirnn0  15742  lgsdinn0  15743  lgseisenlem2  15766  lgseisenlem3  15767  lgsquadlem2  15773  lgsquadlem3  15774  lgsquad2lem1  15776  lgsquad3  15779  2lgslem3  15796  2lgsoddprmlem2  15801  2sqlem4  15813  basvtxval2dom  15851  edgfiedgval2dom  15852  setsvtx  15868  ushgredgedgloop  16042  wlkres  16123  clwwlkccatlem  16143  bj-charfundcALT  16255  1dom1el  16437  pw1ndom3lem  16440  pw1ndom3  16441  2omap  16446  sssneq  16455  0nninf  16458  nnnninfex  16476  nninfnfiinf  16477  trilpolemisumle  16494