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 )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  3eqtr2d  2277  3eqtr2rd  2278  3eqtr4d  2281  3eqtr4rd  2282  3eqtr4a  2297  sbnfc2  3208  ifsbdc  3653  ifeq1dadc  3671  ifeq2dadc  3672  eqifdc  3677  ifnotdc  3679  2if2dc  3680  ifandc  3681  ifordc  3682  ifeqeqxdc  3687  onsucuni2  4711  relop  4930  riinint  5043  iotauni  5350  fniinfv  5761  fsn2  5882  fmptapd  5906  fconst2g  5930  fniunfv  5968  ofres  6317  ofco  6321  caofid1  6331  caofid2  6332  fsuppeq  6487  fsuppeqg  6488  frecsuclem  6677  frecrdg  6679  oasuc  6737  nnacom  6757  nnaass  6758  nndi  6759  nnmass  6760  nnmsucr  6761  nnmcom  6762  funresdfunsndc  6779  uniqs2  6869  en1bg  7087  fundmen  7094  1dom1el  7107  1domsn  7115  pw2f1odclem  7134  mapxpen  7148  xpmapenlem  7149  mapunen  7151  phplem4dom  7163  en2eqpr  7214  sbthlemi5  7278  2omap  7318  omp1eomlem  7434  difinfsnlem  7439  ctmlemr  7448  ctssdccl  7451  ctssdc  7453  infnninf  7464  infnninfOLD  7465  nnnninfeq  7468  pr2cv1  7541  exmidonfinlem  7545  exmidmotap  7627  addcmpblnq  7734  distrnqg  7754  ltexnqq  7775  addcmpblnq0  7810  nqnq0a  7821  nqnq0m  7822  nq0m0r  7823  nq0a0  7824  nnanq0  7825  distrnq0  7826  prarloclemlo  7861  prarloclemcalc  7869  genpassl  7891  genpassu  7892  ltsosr  8131  0idsr  8134  1idsr  8135  mulextsr1lem  8147  cnegex  8505  subsub3  8559  subadd4  8571  mulneg12  8725  mulsub  8729  apreap  8917  cru  8932  recextlem1  8981  cju  9293  ofnegsub  9294  halfaddsub  9543  nn0supp  9623  nneo  9753  zeo2  9756  uzin  9964  xaddcom  10273  xaddass  10281  xleaddadd  10299  iccf1o  10417  fzsuc2  10496  fldiv4lem1div2uz2  10754  flqeqceilz  10768  zmod1congr  10791  modqcyc  10809  modqcyc2  10810  modqaddabs  10812  modqmul1  10827  modqaddmulmod  10841  addmodlteq  10848  frec2uzrdg  10859  frecuzrdgsuctlem  10873  seq3val  10910  seqvalcd  10911  seq3fveq2  10925  seqfveq2g  10927  seq3split  10938  seqsplitg  10939  seqf1oglem2a  10968  seqf1oglem2  10970  seqfeq4g  10981  seq3distr  10982  ser0f  10984  expp1  10996  mulexp  11028  mulexpzap  11029  expadd  11031  expaddzap  11033  expmul  11034  expmulzap  11035  expsubap  11037  expdivap  11040  subsq  11096  mulbinom2  11106  binom3  11107  bernneq  11111  modqexp  11117  nn0opthd  11174  faclbnd  11193  faclbnd6  11196  bccmpl  11206  bcp1n  11213  hashfibclem  11296  hashfibc  11297  hashf1lem1  11299  hashf1  11301  zfz1isolemiso  11305  seq3coll  11308  hashtpglem  11312  ccatsymb  11384  ccatval1lsw  11386  ccatass  11390  eqs1  11410  lswccats1fst  11426  swrdsb0eq  11451  swrdsbslen  11452  swrds1  11454  ccatswrd  11456  pfxres  11467  ccatpfx  11487  pfxpfx  11494  cats1un  11507  swrdccatin1  11511  pfxccatin12  11519  swrdccat  11521  pfxccat3a  11524  swrdccat3b  11526  shftval2  11605  shftval4  11607  seq3shft  11617  crre  11636  remim  11639  remullem  11650  cjexp  11672  sq01  11674  cnrecnv  11690  resqrexlemlo  11793  resqrexlemcalc1  11794  resqrexlemcalc2  11795  resqrexlemcalc3  11796  resqrexlemnm  11798  rsqrmo  11807  abscj  11832  absid  11851  absre  11858  recvalap  11878  maxabsle  11985  maxltsup  11999  2zsupmax  12007  minabs  12017  bdtrilem  12021  bdtri  12022  2zinfmin  12025  xrmaxiflemab  12029  xrmaxiflemcom  12031  xrmaxadd  12043  xrbdtri  12058  iooinsup  12059  climaddc1  12111  climmulc2  12113  climsubc1  12114  climsubc2  12115  climcvg1nlem  12131  summodclem3  12163  zsumdc  12167  isum  12168  isumz  12172  isumss  12174  fisumss  12175  fsum3cvg2  12177  fsumadd  12189  isummulc2  12209  sumsplitdc  12215  fsum2dlemstep  12217  fisumcom2  12221  fisum0diag2  12230  fsumconst  12237  telfsumo  12249  fsumparts  12253  fsumrelem  12254  binomlem  12266  isumshft  12273  isumsplit  12274  arisum  12281  arisum2  12282  trireciplem  12283  geolim2  12295  geo2sum  12297  0.999...  12304  cvgratz  12315  mertensabs  12320  clim2prod  12322  prodf1f  12326  prodmodclem2a  12359  zproddc  12362  iprodap  12363  iprodap0  12365  fprodseq  12366  prod1dc  12369  prodssdc  12372  fprod2dlemstep  12405  fprodcom2fi  12409  fproddivap  12413  ef0lem  12443  efval2  12448  ege2le3  12454  efaddlem  12457  efsub  12464  eftlub  12473  efsep  12474  tanval3ap  12497  efi4p  12500  sinneg  12509  sinmul  12527  sincossq  12531  cos2t  12533  demoivreALT  12557  eirraplem  12560  dvdsmodexp  12578  odd2np1  12656  omoe  12679  divalglemex  12705  divalglemeuneg  12706  divalgmod  12710  flodddiv4  12719  bitsp1  12734  bitsinv1lem  12744  bitsinv1  12745  gcdneg  12775  gcdaddm  12777  modgcd  12784  bezoutlemnewy  12789  gcdass  12808  gcdmultiple  12813  nninfctlemfo  12833  algrp1  12840  lcmneg  12868  lcmgcdeq  12877  lcmass  12879  cncongr2  12898  prmexpb  12946  sqrt2irr  12957  2sqpwodd  12972  qnumdenbi  12988  nn0sqdcq  13004  sqrtrirr  13005  phiprmpw  13020  eulerthlema  13028  fermltl  13032  prmdiveq  13034  modprm0  13053  pythagtriplem1  13064  pythagtriplem12  13074  pythagtriplem14  13076  pythagtriplem15  13077  pythagtriplem16  13078  pythagtriplem17  13079  pythagtriplem19  13081  pcpremul  13092  pcneg  13124  pcgcd  13128  pc2dvds  13129  pcaddlem  13138  pcprod  13145  fldivp1  13147  pcbc  13150  prmpwdvds  13154  pockthlem  13155  mul4sqlem  13192  4sqlem11  13200  4sqlem12  13201  4sqlem17  13206  ballotfilemrv  13312  ballotfilemfg  13318  ballotfilemfrc  13319  ballotfilemrinv0  13325  ctiunctlemfo  13379  ressval3d  13475  resseqnbasd  13476  imasival  13676  qusval  13693  plusfeqg  13733  sgrp1  13775  idmhm  13825  resmhm2  13844  mhmeql  13848  grppropstrg  13873  grpinvinv  13921  grp1  13960  imasgrp2  13962  mulgnngzsum  13979  mulginvcom  13999  mulgnndir  14003  mulgdir  14006  mulgneg2  14008  mulgnnass  14009  mulgass  14011  mulgsubdir  14014  trivsubgd  14052  nmzsubg  14062  qussub  14089  idghm  14111  ablinvadd  14163  ablsub2inv  14164  eqgabl  14183  gzsumgsum  14204  gsump1  14206  gsumconstcmn  14215  prdsval  14222  mgpplusgg  14270  mgpbasg  14273  mgpscag  14275  mgptsetg  14276  mgpdsg  14278  mgpress  14279  srgpcomp  14343  srgpcompp  14344  ringo2times  14382  ring1eq0  14402  ring1  14413  opprmulfvalg  14424  crngoppr  14426  opprsllem  14428  oppr1g  14437  opprunitd  14466  rdivmuldivd  14500  rhmunitinv  14534  scafeqg  14694  lmodvsubval2  14728  lmodsubdi  14730  rmodislmod  14737  sralemg  14824  sraipg  14830  crng2idl  14917  cnfldmulg  14962  cnfldexp  14963  cnfldui  14973  mulgrhm2  14994  zrhrhmb  15006  zlmvscag  15017  znval2  15022  znbaslemnn  15023  znunit  15043  psrval  15099  psrgrp  15125  psrneg  15127  mplval2g  15135  restuni2  15327  lmfval  15343  cnfval  15344  cnpfval  15345  txtopon  15412  txcnp  15421  upxp  15422  txrest  15426  cnmptcom  15448  bl2in  15553  xblss2  15555  isxms2  15602  setsmsdsg  15630  setsmstsetg  15631  metss  15644  resubmet  15706  expcn  15719  cncfcncntop  15743  dvidlemap  15841  dvidrelem  15842  dvidsslem  15843  dvcnp2cntop  15849  dvcoapbr  15857  dvcjbr  15858  dvexp  15861  dvexp2  15862  dvrecap  15863  plyaddlem1  15897  plymullem1  15898  plycolemc  15908  plycjlemc  15910  dvply1  15915  efimpi  15970  tangtx  15989  logdivlti  16033  logfac  16048  cxpexprp  16050  rpcxpsub  16063  rpabscxpbnd  16095  rprelogbdiv  16112  binom4  16138  log2tlbndlog2  16139  birthdaylem2  16145  pellexlem2  16149  mpodvdsmulf1o  16185  0sgmppw  16188  pcbcctr  16201  bcmono  16202  bcp1ctr  16204  bclbnd  16205  bposlem3  16211  lgslem1  16217  lgsmod  16243  lgsdilem  16244  lgsdi  16254  lgsne0  16255  lgsdirnn0  16264  lgsdinn0  16265  lgseisenlem2  16288  lgseisenlem3  16289  lgsquadlem2  16295  lgsquadlem3  16296  lgsquad2lem1  16298  lgsquad3  16301  2lgslem3  16318  2lgsoddprmlem2  16323  2sqlem4  16335  basvtxval2dom  16373  edgfiedgval2dom  16374  setsvtx  16390  ushgredgedgloop  16567  usgr1vr  16587  wlkres  16718  clwwlkccatlem  16739  trlsegvdegfi  16806  eupth2lem3lem2fi  16808  eupth2lem3lem6fi  16810  eupth2lem3lem4fi  16812  depindlem3  16847  bj-charfundcALT  16933  pw1ndom3lem  17117  pw1ndom3  17118  sssneq  17130  0nninf  17145  nnnninfex  17163  nninfnfiinf  17164  repiecele0  17173  trilpolemisumle  17185  qdiff  17196