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 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  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  3189  ifsbdc  3622  ifeq1dadc  3640  ifeq2dadc  3641  eqifdc  3646  ifnotdc  3648  2if2dc  3649  ifandc  3650  ifordc  3651  onsucuni2  4668  relop  4886  riinint  4999  iotauni  5306  fniinfv  5713  fsn2  5829  fmptapd  5853  fconst2g  5877  fniunfv  5913  ofres  6259  ofco  6263  caofid1  6273  caofid2  6274  fsuppeq  6425  fsuppeqg  6426  frecsuclem  6615  frecrdg  6617  oasuc  6675  nnacom  6695  nnaass  6696  nndi  6697  nnmass  6698  nnmsucr  6699  nnmcom  6700  funresdfunsndc  6717  uniqs2  6807  en1bg  7017  fundmen  7024  1dom1el  7036  1domsn  7044  pw2f1odclem  7063  mapxpen  7077  xpmapenlem  7078  phplem4dom  7091  en2eqpr  7142  sbthlemi5  7203  omp1eomlem  7353  difinfsnlem  7358  ctmlemr  7367  ctssdccl  7370  ctssdc  7372  infnninf  7383  infnninfOLD  7384  nnnninfeq  7387  pr2cv1  7460  exmidonfinlem  7464  exmidmotap  7540  addcmpblnq  7647  distrnqg  7667  ltexnqq  7688  addcmpblnq0  7723  nqnq0a  7734  nqnq0m  7735  nq0m0r  7736  nq0a0  7737  nnanq0  7738  distrnq0  7739  prarloclemlo  7774  prarloclemcalc  7782  genpassl  7804  genpassu  7805  ltsosr  8044  0idsr  8047  1idsr  8048  mulextsr1lem  8060  cnegex  8416  subsub3  8470  subadd4  8482  mulneg12  8635  mulsub  8639  apreap  8826  cru  8841  recextlem1  8890  cju  9200  ofnegsub  9201  halfaddsub  9437  nn0supp  9515  nneo  9644  zeo2  9647  uzin  9850  xaddcom  10157  xaddass  10165  xleaddadd  10183  iccf1o  10301  fzsuc2  10376  fldiv4lem1div2uz2  10629  flqeqceilz  10643  zmod1congr  10666  modqcyc  10684  modqcyc2  10685  modqaddabs  10687  modqmul1  10702  modqaddmulmod  10716  addmodlteq  10723  frec2uzrdg  10734  frecuzrdgsuctlem  10748  seq3val  10785  seqvalcd  10786  seq3fveq2  10800  seqfveq2g  10802  seq3split  10813  seqsplitg  10814  seqf1oglem2a  10843  seqf1oglem2  10845  seqfeq4g  10856  seq3distr  10857  ser0f  10859  expp1  10871  mulexp  10903  mulexpzap  10904  expadd  10906  expaddzap  10908  expmul  10909  expmulzap  10910  expsubap  10912  expdivap  10915  subsq  10971  mulbinom2  10981  binom3  10982  bernneq  10985  modqexp  10991  nn0opthd  11047  faclbnd  11066  faclbnd6  11069  bccmpl  11079  bcp1n  11086  zfz1isolemiso  11166  seq3coll  11169  hashtpglem  11173  ccatsymb  11245  ccatval1lsw  11247  ccatass  11251  eqs1  11271  lswccats1fst  11287  swrdsb0eq  11312  swrdsbslen  11313  swrds1  11315  ccatswrd  11317  pfxres  11328  ccatpfx  11348  pfxpfx  11355  cats1un  11368  swrdccatin1  11372  pfxccatin12  11380  swrdccat  11382  pfxccat3a  11385  swrdccat3b  11387  shftval2  11466  shftval4  11468  seq3shft  11478  crre  11497  remim  11500  remullem  11511  cjexp  11533  cnrecnv  11550  resqrexlemlo  11653  resqrexlemcalc1  11654  resqrexlemcalc2  11655  resqrexlemcalc3  11656  resqrexlemnm  11658  rsqrmo  11667  abscj  11692  absid  11711  absre  11717  recvalap  11737  maxabsle  11844  maxltsup  11858  2zsupmax  11866  minabs  11876  bdtrilem  11879  bdtri  11880  2zinfmin  11883  xrmaxiflemab  11887  xrmaxiflemcom  11889  xrmaxadd  11901  xrbdtri  11916  iooinsup  11917  climaddc1  11969  climmulc2  11971  climsubc1  11972  climsubc2  11973  climcvg1nlem  11989  summodclem3  12021  zsumdc  12025  isum  12026  isumz  12030  isumss  12032  fisumss  12033  fsum3cvg2  12035  fsumadd  12047  isummulc2  12067  sumsplitdc  12073  fsum2dlemstep  12075  fisumcom2  12079  fisum0diag2  12088  fsumconst  12095  telfsumo  12107  fsumparts  12111  fsumrelem  12112  binomlem  12124  isumshft  12131  isumsplit  12132  arisum  12139  arisum2  12140  trireciplem  12141  geolim2  12153  geo2sum  12155  0.999...  12162  cvgratz  12173  mertensabs  12178  clim2prod  12180  prodf1f  12184  prodmodclem2a  12217  zproddc  12220  iprodap  12221  iprodap0  12223  fprodseq  12224  prod1dc  12227  prodssdc  12230  fprod2dlemstep  12263  fprodcom2fi  12267  fproddivap  12271  ef0lem  12301  efval2  12306  ege2le3  12312  efaddlem  12315  efsub  12322  eftlub  12331  efsep  12332  tanval3ap  12355  efi4p  12358  sinneg  12367  sinmul  12385  sincossq  12389  cos2t  12391  demoivreALT  12415  eirraplem  12418  dvdsmodexp  12436  odd2np1  12514  omoe  12537  divalglemex  12563  divalglemeuneg  12564  divalgmod  12568  flodddiv4  12577  bitsp1  12592  bitsinv1lem  12602  bitsinv1  12603  gcdneg  12633  gcdaddm  12635  modgcd  12642  bezoutlemnewy  12647  gcdass  12666  gcdmultiple  12671  nninfctlemfo  12691  algrp1  12698  lcmneg  12726  lcmgcdeq  12735  lcmass  12737  cncongr2  12756  prmexpb  12803  sqrt2irr  12814  2sqpwodd  12828  qnumdenbi  12844  phiprmpw  12874  eulerthlema  12882  fermltl  12886  prmdiveq  12888  modprm0  12907  pythagtriplem1  12918  pythagtriplem12  12928  pythagtriplem14  12930  pythagtriplem15  12931  pythagtriplem16  12932  pythagtriplem17  12933  pythagtriplem19  12935  pcpremul  12946  pcneg  12978  pcgcd  12982  pc2dvds  12983  pcaddlem  12992  pcprod  12999  fldivp1  13001  pcbc  13004  prmpwdvds  13008  pockthlem  13009  mul4sqlem  13046  4sqlem11  13054  4sqlem12  13055  4sqlem17  13060  ctiunctlemfo  13140  ressval3d  13235  resseqnbasd  13236  prdsval  13436  imasival  13469  qusval  13486  plusfeqg  13527  sgrp1  13574  idmhm  13632  resmhm2  13651  mhmeql  13655  grppropstrg  13682  grpinvinv  13730  grp1  13769  imasgrp2  13777  mulgnngsum  13794  mulginvcom  13814  mulgnndir  13818  mulgdir  13821  mulgneg2  13823  mulgnnass  13824  mulgass  13826  mulgsubdir  13829  trivsubgd  13867  nmzsubg  13877  qussub  13904  idghm  13926  ablinvadd  13977  ablsub2inv  13978  eqgabl  13997  mgpplusgg  14018  mgpbasg  14020  mgpscag  14021  mgptsetg  14022  mgpdsg  14024  mgpress  14025  srgpcomp  14084  srgpcompp  14085  ringo2times  14122  ring1eq0  14142  ring1  14153  opprmulfvalg  14164  crngoppr  14166  opprsllem  14168  oppr1g  14176  opprunitd  14205  rdivmuldivd  14239  rhmunitinv  14273  scafeqg  14404  lmodvsubval2  14438  lmodsubdi  14440  rmodislmod  14447  sralemg  14534  sraipg  14540  crng2idl  14627  cnfldmulg  14672  cnfldexp  14673  cnfldui  14685  mulgrhm2  14706  zrhrhmb  14718  zlmvscag  14729  znval2  14734  znbaslemnn  14735  znunit  14755  psrval  14762  psrgrp  14786  psrneg  14788  mplval2g  14796  restuni2  14988  lmfval  15004  cnfval  15005  cnpfval  15006  txtopon  15073  txcnp  15082  upxp  15083  txrest  15087  cnmptcom  15109  bl2in  15214  xblss2  15216  isxms2  15263  setsmsdsg  15291  setsmstsetg  15292  metss  15305  resubmet  15367  expcn  15380  cncfcncntop  15404  dvidlemap  15502  dvidrelem  15503  dvidsslem  15504  dvcnp2cntop  15510  dvcoapbr  15518  dvcjbr  15519  dvexp  15522  dvexp2  15523  dvrecap  15524  plyaddlem1  15558  plymullem1  15559  plycolemc  15569  plycjlemc  15571  dvply1  15576  efimpi  15630  tangtx  15649  logdivlti  15692  cxpexprp  15706  rpcxpsub  15719  rpabscxpbnd  15751  rprelogbdiv  15768  binom4  15790  pellexlem2  15792  mpodvdsmulf1o  15804  0sgmppw  15807  lgslem1  15819  lgsmod  15845  lgsdilem  15846  lgsdi  15856  lgsne0  15857  lgsdirnn0  15866  lgsdinn0  15867  lgseisenlem2  15890  lgseisenlem3  15891  lgsquadlem2  15897  lgsquadlem3  15898  lgsquad2lem1  15900  lgsquad3  15903  2lgslem3  15920  2lgsoddprmlem2  15925  2sqlem4  15937  basvtxval2dom  15975  edgfiedgval2dom  15976  setsvtx  15992  ushgredgedgloop  16169  usgr1vr  16189  wlkres  16320  clwwlkccatlem  16341  trlsegvdegfi  16408  eupth2lem3lem2fi  16410  eupth2lem3lem6fi  16412  eupth2lem3lem4fi  16414  depindlem3  16449  bj-charfundcALT  16525  pw1ndom3lem  16709  pw1ndom3  16710  2omap  16715  sssneq  16724  0nninf  16730  nnnninfex  16748  nninfnfiinf  16749  repiecele0  16758  trilpolemisumle  16770  qdiff  16781  gsumgfsum  16813  gfsump1  16815