Theorem eqtr4d 2267

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

Syntax hints:   -> wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  3eqtr2d  2270  3eqtr2rd  2271  3eqtr4d  2274  3eqtr4rd  2275  3eqtr4a  2290  sbnfc2  3188  ifsbdc  3618  ifeq1dadc  3636  ifeq2dadc  3637  eqifdc  3642  ifnotdc  3644  2if2dc  3645  ifandc  3646  ifordc  3647  onsucuni2  4662  relop  4880  riinint  4993  iotauni  5299  fniinfv  5704  fsn2  5821  fmptapd  5845  fconst2g  5869  fniunfv  5903  ofres  6250  ofco  6254  caofid1  6264  caofid2  6265  frecsuclem  6572  frecrdg  6574  oasuc  6632  nnacom  6652  nnaass  6653  nndi  6654  nnmass  6655  nnmsucr  6656  nnmcom  6657  funresdfunsndc  6674  uniqs2  6764  en1bg  6974  fundmen  6981  1dom1el  6993  1domsn  7001  pw2f1odclem  7020  mapxpen  7034  xpmapenlem  7035  phplem4dom  7048  en2eqpr  7099  sbthlemi5  7160  omp1eomlem  7293  difinfsnlem  7298  ctmlemr  7307  ctssdccl  7310  ctssdc  7312  infnninf  7323  infnninfOLD  7324  nnnninfeq  7327  pr2cv1  7400  exmidonfinlem  7404  exmidmotap  7480  addcmpblnq  7587  distrnqg  7607  ltexnqq  7628  addcmpblnq0  7663  nqnq0a  7674  nqnq0m  7675  nq0m0r  7676  nq0a0  7677  nnanq0  7678  distrnq0  7679  prarloclemlo  7714  prarloclemcalc  7722  genpassl  7744  genpassu  7745  ltsosr  7984  0idsr  7987  1idsr  7988  mulextsr1lem  8000  cnegex  8357  subsub3  8411  subadd4  8423  mulneg12  8576  mulsub  8580  apreap  8767  cru  8782  recextlem1  8831  cju  9141  ofnegsub  9142  halfaddsub  9378  nn0supp  9454  nneo  9583  zeo2  9586  uzin  9789  xaddcom  10096  xaddass  10104  xleaddadd  10122  iccf1o  10239  fzsuc2  10314  fldiv4lem1div2uz2  10567  flqeqceilz  10581  zmod1congr  10604  modqcyc  10622  modqcyc2  10623  modqaddabs  10625  modqmul1  10640  modqaddmulmod  10654  addmodlteq  10661  frec2uzrdg  10672  frecuzrdgsuctlem  10686  seq3val  10723  seqvalcd  10724  seq3fveq2  10738  seqfveq2g  10740  seq3split  10751  seqsplitg  10752  seqf1oglem2a  10781  seqf1oglem2  10783  seqfeq4g  10794  seq3distr  10795  ser0f  10797  expp1  10809  mulexp  10841  mulexpzap  10842  expadd  10844  expaddzap  10846  expmul  10847  expmulzap  10848  expsubap  10850  expdivap  10853  subsq  10909  mulbinom2  10919  binom3  10920  bernneq  10923  modqexp  10929  nn0opthd  10985  faclbnd  11004  faclbnd6  11007  bccmpl  11017  bcp1n  11024  zfz1isolemiso  11104  seq3coll  11107  hashtpglem  11111  ccatsymb  11183  ccatval1lsw  11185  ccatass  11189  eqs1  11209  lswccats1fst  11225  swrdsb0eq  11250  swrdsbslen  11251  swrds1  11253  ccatswrd  11255  pfxres  11266  ccatpfx  11286  pfxpfx  11293  cats1un  11306  swrdccatin1  11310  pfxccatin12  11318  swrdccat  11320  pfxccat3a  11323  swrdccat3b  11325  shftval2  11404  shftval4  11406  seq3shft  11416  crre  11435  remim  11438  remullem  11449  cjexp  11471  cnrecnv  11488  resqrexlemlo  11591  resqrexlemcalc1  11592  resqrexlemcalc2  11593  resqrexlemcalc3  11594  resqrexlemnm  11596  rsqrmo  11605  abscj  11630  absid  11649  absre  11655  recvalap  11675  maxabsle  11782  maxltsup  11796  2zsupmax  11804  minabs  11814  bdtrilem  11817  bdtri  11818  2zinfmin  11821  xrmaxiflemab  11825  xrmaxiflemcom  11827  xrmaxadd  11839  xrbdtri  11854  iooinsup  11855  climaddc1  11907  climmulc2  11909  climsubc1  11910  climsubc2  11911  climcvg1nlem  11927  summodclem3  11959  zsumdc  11963  isum  11964  isumz  11968  isumss  11970  fisumss  11971  fsum3cvg2  11973  fsumadd  11985  isummulc2  12005  sumsplitdc  12011  fsum2dlemstep  12013  fisumcom2  12017  fisum0diag2  12026  fsumconst  12033  telfsumo  12045  fsumparts  12049  fsumrelem  12050  binomlem  12062  isumshft  12069  isumsplit  12070  arisum  12077  arisum2  12078  trireciplem  12079  geolim2  12091  geo2sum  12093  0.999...  12100  cvgratz  12111  mertensabs  12116  clim2prod  12118  prodf1f  12122  prodmodclem2a  12155  zproddc  12158  iprodap  12159  iprodap0  12161  fprodseq  12162  prod1dc  12165  prodssdc  12168  fprod2dlemstep  12201  fprodcom2fi  12205  fproddivap  12209  ef0lem  12239  efval2  12244  ege2le3  12250  efaddlem  12253  efsub  12260  eftlub  12269  efsep  12270  tanval3ap  12293  efi4p  12296  sinneg  12305  sinmul  12323  sincossq  12327  cos2t  12329  demoivreALT  12353  eirraplem  12356  dvdsmodexp  12374  odd2np1  12452  omoe  12475  divalglemex  12501  divalglemeuneg  12502  divalgmod  12506  flodddiv4  12515  bitsp1  12530  bitsinv1lem  12540  bitsinv1  12541  gcdneg  12571  gcdaddm  12573  modgcd  12580  bezoutlemnewy  12585  gcdass  12604  gcdmultiple  12609  nninfctlemfo  12629  algrp1  12636  lcmneg  12664  lcmgcdeq  12673  lcmass  12675  cncongr2  12694  prmexpb  12741  sqrt2irr  12752  2sqpwodd  12766  qnumdenbi  12782  phiprmpw  12812  eulerthlema  12820  fermltl  12824  prmdiveq  12826  modprm0  12845  pythagtriplem1  12856  pythagtriplem12  12866  pythagtriplem14  12868  pythagtriplem15  12869  pythagtriplem16  12870  pythagtriplem17  12871  pythagtriplem19  12873  pcpremul  12884  pcneg  12916  pcgcd  12920  pc2dvds  12921  pcaddlem  12930  pcprod  12937  fldivp1  12939  pcbc  12942  prmpwdvds  12946  pockthlem  12947  mul4sqlem  12984  4sqlem11  12992  4sqlem12  12993  4sqlem17  12998  ctiunctlemfo  13078  ressval3d  13173  resseqnbasd  13174  prdsval  13374  imasival  13407  qusval  13424  plusfeqg  13465  sgrp1  13512  idmhm  13570  resmhm2  13589  mhmeql  13593  grppropstrg  13620  grpinvinv  13668  grp1  13707  imasgrp2  13715  mulgnngsum  13732  mulginvcom  13752  mulgnndir  13756  mulgdir  13759  mulgneg2  13761  mulgnnass  13762  mulgass  13764  mulgsubdir  13767  trivsubgd  13805  nmzsubg  13815  qussub  13842  idghm  13864  ablinvadd  13915  ablsub2inv  13916  eqgabl  13935  mgpplusgg  13956  mgpbasg  13958  mgpscag  13959  mgptsetg  13960  mgpdsg  13962  mgpress  13963  srgpcomp  14022  srgpcompp  14023  ringo2times  14060  ring1eq0  14080  ring1  14091  opprmulfvalg  14102  crngoppr  14104  opprsllem  14106  oppr1g  14114  opprunitd  14143  rdivmuldivd  14177  rhmunitinv  14211  scafeqg  14341  lmodvsubval2  14375  lmodsubdi  14377  rmodislmod  14384  sralemg  14471  sraipg  14477  crng2idl  14564  cnfldmulg  14609  cnfldexp  14610  cnfldui  14622  mulgrhm2  14643  zrhrhmb  14655  zlmvscag  14666  znval2  14671  znbaslemnn  14672  znunit  14692  psrval  14699  psrgrp  14718  psrneg  14720  mplval2g  14728  restuni2  14920  lmfval  14936  cnfval  14937  cnpfval  14938  txtopon  15005  txcnp  15014  upxp  15015  txrest  15019  cnmptcom  15041  bl2in  15146  xblss2  15148  isxms2  15195  setsmsdsg  15223  setsmstsetg  15224  metss  15237  resubmet  15299  expcn  15312  cncfcncntop  15336  dvidlemap  15434  dvidrelem  15435  dvidsslem  15436  dvcnp2cntop  15442  dvcoapbr  15450  dvcjbr  15451  dvexp  15454  dvexp2  15455  dvrecap  15456  plyaddlem1  15490  plymullem1  15491  plycolemc  15501  plycjlemc  15503  dvply1  15508  efimpi  15562  tangtx  15581  logdivlti  15624  cxpexprp  15638  rpcxpsub  15651  rpabscxpbnd  15683  rprelogbdiv  15700  binom4  15722  mpodvdsmulf1o  15733  0sgmppw  15736  lgslem1  15748  lgsmod  15774  lgsdilem  15775  lgsdi  15785  lgsne0  15786  lgsdirnn0  15795  lgsdinn0  15796  lgseisenlem2  15819  lgseisenlem3  15820  lgsquadlem2  15826  lgsquadlem3  15827  lgsquad2lem1  15829  lgsquad3  15832  2lgslem3  15849  2lgsoddprmlem2  15854  2sqlem4  15866  basvtxval2dom  15904  edgfiedgval2dom  15905  setsvtx  15921  ushgredgedgloop  16098  usgr1vr  16118  wlkres  16249  clwwlkccatlem  16270  trlsegvdegfi  16337  eupth2lem3lem2fi  16339  eupth2lem3lem6fi  16341  eupth2lem3lem4fi  16343  depindlem3  16378  bj-charfundcALT  16455  pw1ndom3lem  16639  pw1ndom3  16640  2omap  16645  sssneq  16654  0nninf  16657  nnnninfex  16675  nninfnfiinf  16676  trilpolemisumle  16693  qdiff  16704  gsumgfsum  16736  gfsump1  16738