Theorem eqtr4d 2274

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

Syntax hints:   -> wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  3eqtr2d  2277  3eqtr2rd  2278  3eqtr4d  2281  3eqtr4rd  2282  3eqtr4a  2297  sbnfc2  3208  ifsbdc  3650  ifeq1dadc  3668  ifeq2dadc  3669  eqifdc  3674  ifnotdc  3676  2if2dc  3677  ifandc  3678  ifordc  3679  ifeqeqxdc  3684  onsucuni2  4706  relop  4925  riinint  5038  iotauni  5345  fniinfv  5755  fsn2  5873  fmptapd  5897  fconst2g  5921  fniunfv  5958  ofres  6307  ofco  6311  caofid1  6321  caofid2  6322  fsuppeq  6477  fsuppeqg  6478  frecsuclem  6667  frecrdg  6669  oasuc  6727  nnacom  6747  nnaass  6748  nndi  6749  nnmass  6750  nnmsucr  6751  nnmcom  6752  funresdfunsndc  6769  uniqs2  6859  en1bg  7077  fundmen  7084  1dom1el  7097  1domsn  7105  pw2f1odclem  7124  mapxpen  7138  xpmapenlem  7139  mapunen  7141  phplem4dom  7153  en2eqpr  7204  sbthlemi5  7268  2omap  7308  omp1eomlem  7424  difinfsnlem  7429  ctmlemr  7438  ctssdccl  7441  ctssdc  7443  infnninf  7454  infnninfOLD  7455  nnnninfeq  7458  pr2cv1  7531  exmidonfinlem  7535  exmidmotap  7617  addcmpblnq  7724  distrnqg  7744  ltexnqq  7765  addcmpblnq0  7800  nqnq0a  7811  nqnq0m  7812  nq0m0r  7813  nq0a0  7814  nnanq0  7815  distrnq0  7816  prarloclemlo  7851  prarloclemcalc  7859  genpassl  7881  genpassu  7882  ltsosr  8121  0idsr  8124  1idsr  8125  mulextsr1lem  8137  cnegex  8494  subsub3  8548  subadd4  8560  mulneg12  8714  mulsub  8718  apreap  8905  cru  8920  recextlem1  8969  cju  9281  ofnegsub  9282  halfaddsub  9518  nn0supp  9598  nneo  9728  zeo2  9731  uzin  9934  xaddcom  10242  xaddass  10250  xleaddadd  10268  iccf1o  10386  fzsuc2  10464  fldiv4lem1div2uz2  10719  flqeqceilz  10733  zmod1congr  10756  modqcyc  10774  modqcyc2  10775  modqaddabs  10777  modqmul1  10792  modqaddmulmod  10806  addmodlteq  10813  frec2uzrdg  10824  frecuzrdgsuctlem  10838  seq3val  10875  seqvalcd  10876  seq3fveq2  10890  seqfveq2g  10892  seq3split  10903  seqsplitg  10904  seqf1oglem2a  10933  seqf1oglem2  10935  seqfeq4g  10946  seq3distr  10947  ser0f  10949  expp1  10961  mulexp  10993  mulexpzap  10994  expadd  10996  expaddzap  10998  expmul  10999  expmulzap  11000  expsubap  11002  expdivap  11005  subsq  11061  mulbinom2  11071  binom3  11072  bernneq  11076  modqexp  11082  nn0opthd  11138  faclbnd  11157  faclbnd6  11160  bccmpl  11170  bcp1n  11177  hashfibclem  11260  hashfibc  11261  hashf1lem1  11263  hashf1  11265  zfz1isolemiso  11269  seq3coll  11272  hashtpglem  11276  ccatsymb  11348  ccatval1lsw  11350  ccatass  11354  eqs1  11374  lswccats1fst  11390  swrdsb0eq  11415  swrdsbslen  11416  swrds1  11418  ccatswrd  11420  pfxres  11431  ccatpfx  11451  pfxpfx  11458  cats1un  11471  swrdccatin1  11475  pfxccatin12  11483  swrdccat  11485  pfxccat3a  11488  swrdccat3b  11490  shftval2  11569  shftval4  11571  seq3shft  11581  crre  11600  remim  11603  remullem  11614  cjexp  11636  sq01  11638  cnrecnv  11654  resqrexlemlo  11757  resqrexlemcalc1  11758  resqrexlemcalc2  11759  resqrexlemcalc3  11760  resqrexlemnm  11762  rsqrmo  11771  abscj  11796  absid  11815  absre  11821  recvalap  11841  maxabsle  11948  maxltsup  11962  2zsupmax  11970  minabs  11980  bdtrilem  11983  bdtri  11984  2zinfmin  11987  xrmaxiflemab  11991  xrmaxiflemcom  11993  xrmaxadd  12005  xrbdtri  12020  iooinsup  12021  climaddc1  12073  climmulc2  12075  climsubc1  12076  climsubc2  12077  climcvg1nlem  12093  summodclem3  12125  zsumdc  12129  isum  12130  isumz  12134  isumss  12136  fisumss  12137  fsum3cvg2  12139  fsumadd  12151  isummulc2  12171  sumsplitdc  12177  fsum2dlemstep  12179  fisumcom2  12183  fisum0diag2  12192  fsumconst  12199  telfsumo  12211  fsumparts  12215  fsumrelem  12216  binomlem  12228  isumshft  12235  isumsplit  12236  arisum  12243  arisum2  12244  trireciplem  12245  geolim2  12257  geo2sum  12259  0.999...  12266  cvgratz  12277  mertensabs  12282  clim2prod  12284  prodf1f  12288  prodmodclem2a  12321  zproddc  12324  iprodap  12325  iprodap0  12327  fprodseq  12328  prod1dc  12331  prodssdc  12334  fprod2dlemstep  12367  fprodcom2fi  12371  fproddivap  12375  ef0lem  12405  efval2  12410  ege2le3  12416  efaddlem  12419  efsub  12426  eftlub  12435  efsep  12436  tanval3ap  12459  efi4p  12462  sinneg  12471  sinmul  12489  sincossq  12493  cos2t  12495  demoivreALT  12519  eirraplem  12522  dvdsmodexp  12540  odd2np1  12618  omoe  12641  divalglemex  12667  divalglemeuneg  12668  divalgmod  12672  flodddiv4  12681  bitsp1  12696  bitsinv1lem  12706  bitsinv1  12707  gcdneg  12737  gcdaddm  12739  modgcd  12746  bezoutlemnewy  12751  gcdass  12770  gcdmultiple  12775  nninfctlemfo  12795  algrp1  12802  lcmneg  12830  lcmgcdeq  12839  lcmass  12841  cncongr2  12860  prmexpb  12907  sqrt2irr  12918  2sqpwodd  12932  qnumdenbi  12948  phiprmpw  12978  eulerthlema  12986  fermltl  12990  prmdiveq  12992  modprm0  13011  pythagtriplem1  13022  pythagtriplem12  13032  pythagtriplem14  13034  pythagtriplem15  13035  pythagtriplem16  13036  pythagtriplem17  13037  pythagtriplem19  13039  pcpremul  13050  pcneg  13082  pcgcd  13086  pc2dvds  13087  pcaddlem  13096  pcprod  13103  fldivp1  13105  pcbc  13108  prmpwdvds  13112  pockthlem  13113  mul4sqlem  13150  4sqlem11  13158  4sqlem12  13159  4sqlem17  13164  ballotfilemrv  13241  ballotfilemfg  13247  ballotfilemfrc  13248  ballotfilemrinv0  13254  ctiunctlemfo  13308  ressval3d  13403  resseqnbasd  13404  imasival  13604  qusval  13621  plusfeqg  13661  sgrp1  13703  idmhm  13753  resmhm2  13772  mhmeql  13776  grppropstrg  13801  grpinvinv  13849  grp1  13888  imasgrp2  13890  mulgnngzsum  13907  mulginvcom  13927  mulgnndir  13931  mulgdir  13934  mulgneg2  13936  mulgnnass  13937  mulgass  13939  mulgsubdir  13942  trivsubgd  13980  nmzsubg  13990  qussub  14017  idghm  14039  ablinvadd  14091  ablsub2inv  14092  eqgabl  14111  gzsumgsum  14132  gsump1  14134  gsumconstcmn  14143  prdsval  14150  mgpplusgg  14198  mgpbasg  14200  mgpscag  14201  mgptsetg  14202  mgpdsg  14204  mgpress  14205  srgpcomp  14268  srgpcompp  14269  ringo2times  14306  ring1eq0  14326  ring1  14337  opprmulfvalg  14348  crngoppr  14350  opprsllem  14352  oppr1g  14361  opprunitd  14390  rdivmuldivd  14424  rhmunitinv  14458  scafeqg  14617  lmodvsubval2  14651  lmodsubdi  14653  rmodislmod  14660  sralemg  14747  sraipg  14753  crng2idl  14840  cnfldmulg  14885  cnfldexp  14886  cnfldui  14896  mulgrhm2  14917  zrhrhmb  14929  zlmvscag  14940  znval2  14945  znbaslemnn  14946  znunit  14966  psrval  14973  psrgrp  14999  psrneg  15001  mplval2g  15009  restuni2  15201  lmfval  15217  cnfval  15218  cnpfval  15219  txtopon  15286  txcnp  15295  upxp  15296  txrest  15300  cnmptcom  15322  bl2in  15427  xblss2  15429  isxms2  15476  setsmsdsg  15504  setsmstsetg  15505  metss  15518  resubmet  15580  expcn  15593  cncfcncntop  15617  dvidlemap  15715  dvidrelem  15716  dvidsslem  15717  dvcnp2cntop  15723  dvcoapbr  15731  dvcjbr  15732  dvexp  15735  dvexp2  15736  dvrecap  15737  plyaddlem1  15771  plymullem1  15772  plycolemc  15782  plycjlemc  15784  dvply1  15789  efimpi  15843  tangtx  15862  logdivlti  15905  logfac  15918  cxpexprp  15920  rpcxpsub  15933  rpabscxpbnd  15965  rprelogbdiv  15982  binom4  16004  pellexlem2  16006  mpodvdsmulf1o  16018  0sgmppw  16021  lgslem1  16033  lgsmod  16059  lgsdilem  16060  lgsdi  16070  lgsne0  16071  lgsdirnn0  16080  lgsdinn0  16081  lgseisenlem2  16104  lgseisenlem3  16105  lgsquadlem2  16111  lgsquadlem3  16112  lgsquad2lem1  16114  lgsquad3  16117  2lgslem3  16134  2lgsoddprmlem2  16139  2sqlem4  16151  basvtxval2dom  16189  edgfiedgval2dom  16190  setsvtx  16206  ushgredgedgloop  16383  usgr1vr  16403  wlkres  16534  clwwlkccatlem  16555  trlsegvdegfi  16622  eupth2lem3lem2fi  16624  eupth2lem3lem6fi  16626  eupth2lem3lem4fi  16628  depindlem3  16663  bj-charfundcALT  16749  pw1ndom3lem  16933  pw1ndom3  16934  sssneq  16946  0nninf  16952  nnnninfex  16970  nninfnfiinf  16971  repiecele0  16980  trilpolemisumle  16992  qdiff  17003