Theorem eqtr4d 2270

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 2240	. 2 |- ( ph -> B = C )
4	1, 3	eqtrd 2267	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 2216

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

This theorem is referenced by:  3eqtr2d  2273  3eqtr2rd  2274  3eqtr4d  2277  3eqtr4rd  2278  3eqtr4a  2293  sbnfc2  3202  ifsbdc  3639  ifeq1dadc  3657  ifeq2dadc  3658  eqifdc  3663  ifnotdc  3665  2if2dc  3666  ifandc  3667  ifordc  3668  ifeqeqxdc  3673  onsucuni2  4691  relop  4910  riinint  5023  iotauni  5330  fniinfv  5740  fsn2  5856  fmptapd  5880  fconst2g  5904  fniunfv  5941  ofres  6290  ofco  6294  caofid1  6304  caofid2  6305  fsuppeq  6460  fsuppeqg  6461  frecsuclem  6650  frecrdg  6652  oasuc  6710  nnacom  6730  nnaass  6731  nndi  6732  nnmass  6733  nnmsucr  6734  nnmcom  6735  funresdfunsndc  6752  uniqs2  6842  en1bg  7053  fundmen  7060  1dom1el  7073  1domsn  7081  pw2f1odclem  7100  mapxpen  7114  xpmapenlem  7115  mapunen  7117  phplem4dom  7129  en2eqpr  7180  sbthlemi5  7244  2omap  7282  omp1eomlem  7398  difinfsnlem  7403  ctmlemr  7412  ctssdccl  7415  ctssdc  7417  infnninf  7428  infnninfOLD  7429  nnnninfeq  7432  pr2cv1  7505  exmidonfinlem  7509  exmidmotap  7591  addcmpblnq  7698  distrnqg  7718  ltexnqq  7739  addcmpblnq0  7774  nqnq0a  7785  nqnq0m  7786  nq0m0r  7787  nq0a0  7788  nnanq0  7789  distrnq0  7790  prarloclemlo  7825  prarloclemcalc  7833  genpassl  7855  genpassu  7856  ltsosr  8095  0idsr  8098  1idsr  8099  mulextsr1lem  8111  cnegex  8467  subsub3  8521  subadd4  8533  mulneg12  8687  mulsub  8691  apreap  8878  cru  8893  recextlem1  8942  cju  9252  ofnegsub  9253  halfaddsub  9489  nn0supp  9569  nneo  9699  zeo2  9702  uzin  9905  xaddcom  10213  xaddass  10221  xleaddadd  10239  iccf1o  10357  fzsuc2  10435  fldiv4lem1div2uz2  10690  flqeqceilz  10704  zmod1congr  10727  modqcyc  10745  modqcyc2  10746  modqaddabs  10748  modqmul1  10763  modqaddmulmod  10777  addmodlteq  10784  frec2uzrdg  10795  frecuzrdgsuctlem  10809  seq3val  10846  seqvalcd  10847  seq3fveq2  10861  seqfveq2g  10863  seq3split  10874  seqsplitg  10875  seqf1oglem2a  10904  seqf1oglem2  10906  seqfeq4g  10917  seq3distr  10918  ser0f  10920  expp1  10932  mulexp  10964  mulexpzap  10965  expadd  10967  expaddzap  10969  expmul  10970  expmulzap  10971  expsubap  10973  expdivap  10976  subsq  11032  mulbinom2  11042  binom3  11043  bernneq  11047  modqexp  11053  nn0opthd  11109  faclbnd  11128  faclbnd6  11131  bccmpl  11141  bcp1n  11148  hashfibclem  11231  hashfibc  11232  zfz1isolemiso  11236  seq3coll  11239  hashtpglem  11243  ccatsymb  11315  ccatval1lsw  11317  ccatass  11321  eqs1  11341  lswccats1fst  11357  swrdsb0eq  11382  swrdsbslen  11383  swrds1  11385  ccatswrd  11387  pfxres  11398  ccatpfx  11418  pfxpfx  11425  cats1un  11438  swrdccatin1  11442  pfxccatin12  11450  swrdccat  11452  pfxccat3a  11455  swrdccat3b  11457  shftval2  11536  shftval4  11538  seq3shft  11548  crre  11567  remim  11570  remullem  11581  cjexp  11603  cnrecnv  11620  resqrexlemlo  11723  resqrexlemcalc1  11724  resqrexlemcalc2  11725  resqrexlemcalc3  11726  resqrexlemnm  11728  rsqrmo  11737  abscj  11762  absid  11781  absre  11787  recvalap  11807  maxabsle  11914  maxltsup  11928  2zsupmax  11936  minabs  11946  bdtrilem  11949  bdtri  11950  2zinfmin  11953  xrmaxiflemab  11957  xrmaxiflemcom  11959  xrmaxadd  11971  xrbdtri  11986  iooinsup  11987  climaddc1  12039  climmulc2  12041  climsubc1  12042  climsubc2  12043  climcvg1nlem  12059  summodclem3  12091  zsumdc  12095  isum  12096  isumz  12100  isumss  12102  fisumss  12103  fsum3cvg2  12105  fsumadd  12117  isummulc2  12137  sumsplitdc  12143  fsum2dlemstep  12145  fisumcom2  12149  fisum0diag2  12158  fsumconst  12165  telfsumo  12177  fsumparts  12181  fsumrelem  12182  binomlem  12194  isumshft  12201  isumsplit  12202  arisum  12209  arisum2  12210  trireciplem  12211  geolim2  12223  geo2sum  12225  0.999...  12232  cvgratz  12243  mertensabs  12248  clim2prod  12250  prodf1f  12254  prodmodclem2a  12287  zproddc  12290  iprodap  12291  iprodap0  12293  fprodseq  12294  prod1dc  12297  prodssdc  12300  fprod2dlemstep  12333  fprodcom2fi  12337  fproddivap  12341  ef0lem  12371  efval2  12376  ege2le3  12382  efaddlem  12385  efsub  12392  eftlub  12401  efsep  12402  tanval3ap  12425  efi4p  12428  sinneg  12437  sinmul  12455  sincossq  12459  cos2t  12461  demoivreALT  12485  eirraplem  12488  dvdsmodexp  12506  odd2np1  12584  omoe  12607  divalglemex  12633  divalglemeuneg  12634  divalgmod  12638  flodddiv4  12647  bitsp1  12662  bitsinv1lem  12672  bitsinv1  12673  gcdneg  12703  gcdaddm  12705  modgcd  12712  bezoutlemnewy  12717  gcdass  12736  gcdmultiple  12741  nninfctlemfo  12761  algrp1  12768  lcmneg  12796  lcmgcdeq  12805  lcmass  12807  cncongr2  12826  prmexpb  12873  sqrt2irr  12884  2sqpwodd  12898  qnumdenbi  12914  phiprmpw  12944  eulerthlema  12952  fermltl  12956  prmdiveq  12958  modprm0  12977  pythagtriplem1  12988  pythagtriplem12  12998  pythagtriplem14  13000  pythagtriplem15  13001  pythagtriplem16  13002  pythagtriplem17  13003  pythagtriplem19  13005  pcpremul  13016  pcneg  13048  pcgcd  13052  pc2dvds  13053  pcaddlem  13062  pcprod  13069  fldivp1  13071  pcbc  13074  prmpwdvds  13078  pockthlem  13079  mul4sqlem  13116  4sqlem11  13124  4sqlem12  13125  4sqlem17  13130  ballotfilemrv  13207  ballotfilemfg  13213  ballotfilemfrc  13214  ballotfilemrinv0  13220  ctiunctlemfo  13274  ressval3d  13369  resseqnbasd  13370  imasival  13570  qusval  13587  plusfeqg  13627  sgrp1  13674  idmhm  13724  resmhm2  13743  mhmeql  13747  grppropstrg  13774  grpinvinv  13822  grp1  13861  imasgrp2  13863  mulgnngsum  13880  mulginvcom  13900  mulgnndir  13904  mulgdir  13907  mulgneg2  13909  mulgnnass  13910  mulgass  13912  mulgsubdir  13915  trivsubgd  13953  nmzsubg  13963  qussub  13990  idghm  14012  ablinvadd  14063  ablsub2inv  14064  eqgabl  14083  gsumgfsum  14106  gfsump1  14108  prdsval  14115  mgpplusgg  14163  mgpbasg  14165  mgpscag  14166  mgptsetg  14167  mgpdsg  14169  mgpress  14170  srgpcomp  14233  srgpcompp  14234  ringo2times  14271  ring1eq0  14291  ring1  14302  opprmulfvalg  14313  crngoppr  14315  opprsllem  14317  oppr1g  14326  opprunitd  14355  rdivmuldivd  14389  rhmunitinv  14423  scafeqg  14582  lmodvsubval2  14616  lmodsubdi  14618  rmodislmod  14625  sralemg  14712  sraipg  14718  crng2idl  14805  cnfldmulg  14850  cnfldexp  14851  cnfldui  14863  mulgrhm2  14884  zrhrhmb  14896  zlmvscag  14907  znval2  14912  znbaslemnn  14913  znunit  14933  psrval  14940  psrgrp  14966  psrneg  14968  mplval2g  14976  restuni2  15168  lmfval  15184  cnfval  15185  cnpfval  15186  txtopon  15253  txcnp  15262  upxp  15263  txrest  15267  cnmptcom  15289  bl2in  15394  xblss2  15396  isxms2  15443  setsmsdsg  15471  setsmstsetg  15472  metss  15485  resubmet  15547  expcn  15560  cncfcncntop  15584  dvidlemap  15682  dvidrelem  15683  dvidsslem  15684  dvcnp2cntop  15690  dvcoapbr  15698  dvcjbr  15699  dvexp  15702  dvexp2  15703  dvrecap  15704  plyaddlem1  15738  plymullem1  15739  plycolemc  15749  plycjlemc  15751  dvply1  15756  efimpi  15810  tangtx  15829  logdivlti  15872  cxpexprp  15886  rpcxpsub  15899  rpabscxpbnd  15931  rprelogbdiv  15948  binom4  15970  pellexlem2  15972  mpodvdsmulf1o  15984  0sgmppw  15987  lgslem1  15999  lgsmod  16025  lgsdilem  16026  lgsdi  16036  lgsne0  16037  lgsdirnn0  16046  lgsdinn0  16047  lgseisenlem2  16070  lgseisenlem3  16071  lgsquadlem2  16077  lgsquadlem3  16078  lgsquad2lem1  16080  lgsquad3  16083  2lgslem3  16100  2lgsoddprmlem2  16105  2sqlem4  16117  basvtxval2dom  16155  edgfiedgval2dom  16156  setsvtx  16172  ushgredgedgloop  16349  usgr1vr  16369  wlkres  16500  clwwlkccatlem  16521  trlsegvdegfi  16588  eupth2lem3lem2fi  16590  eupth2lem3lem6fi  16592  eupth2lem3lem4fi  16594  depindlem3  16629  bj-charfundcALT  16705  pw1ndom3lem  16889  pw1ndom3  16890  sssneq  16902  0nninf  16908  nnnninfex  16926  nninfnfiinf  16927  repiecele0  16936  trilpolemisumle  16948  qdiff  16959