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  8504  subsub3  8558  subadd4  8570  mulneg12  8724  mulsub  8728  apreap  8915  cru  8930  recextlem1  8979  cju  9291  ofnegsub  9292  halfaddsub  9539  nn0supp  9619  nneo  9749  zeo2  9752  uzin  9955  xaddcom  10263  xaddass  10271  xleaddadd  10289  iccf1o  10407  fzsuc2  10486  fldiv4lem1div2uz2  10741  flqeqceilz  10755  zmod1congr  10778  modqcyc  10796  modqcyc2  10797  modqaddabs  10799  modqmul1  10814  modqaddmulmod  10828  addmodlteq  10835  frec2uzrdg  10846  frecuzrdgsuctlem  10860  seq3val  10897  seqvalcd  10898  seq3fveq2  10912  seqfveq2g  10914  seq3split  10925  seqsplitg  10926  seqf1oglem2a  10955  seqf1oglem2  10957  seqfeq4g  10968  seq3distr  10969  ser0f  10971  expp1  10983  mulexp  11015  mulexpzap  11016  expadd  11018  expaddzap  11020  expmul  11021  expmulzap  11022  expsubap  11024  expdivap  11027  subsq  11083  mulbinom2  11093  binom3  11094  bernneq  11098  modqexp  11104  nn0opthd  11160  faclbnd  11179  faclbnd6  11182  bccmpl  11192  bcp1n  11199  hashfibclem  11282  hashfibc  11283  hashf1lem1  11285  hashf1  11287  zfz1isolemiso  11291  seq3coll  11294  hashtpglem  11298  ccatsymb  11370  ccatval1lsw  11372  ccatass  11376  eqs1  11396  lswccats1fst  11412  swrdsb0eq  11437  swrdsbslen  11438  swrds1  11440  ccatswrd  11442  pfxres  11453  ccatpfx  11473  pfxpfx  11480  cats1un  11493  swrdccatin1  11497  pfxccatin12  11505  swrdccat  11507  pfxccat3a  11510  swrdccat3b  11512  shftval2  11591  shftval4  11593  seq3shft  11603  crre  11622  remim  11625  remullem  11636  cjexp  11658  sq01  11660  cnrecnv  11676  resqrexlemlo  11779  resqrexlemcalc1  11780  resqrexlemcalc2  11781  resqrexlemcalc3  11782  resqrexlemnm  11784  rsqrmo  11793  abscj  11818  absid  11837  absre  11843  recvalap  11863  maxabsle  11970  maxltsup  11984  2zsupmax  11992  minabs  12002  bdtrilem  12005  bdtri  12006  2zinfmin  12009  xrmaxiflemab  12013  xrmaxiflemcom  12015  xrmaxadd  12027  xrbdtri  12042  iooinsup  12043  climaddc1  12095  climmulc2  12097  climsubc1  12098  climsubc2  12099  climcvg1nlem  12115  summodclem3  12147  zsumdc  12151  isum  12152  isumz  12156  isumss  12158  fisumss  12159  fsum3cvg2  12161  fsumadd  12173  isummulc2  12193  sumsplitdc  12199  fsum2dlemstep  12201  fisumcom2  12205  fisum0diag2  12214  fsumconst  12221  telfsumo  12233  fsumparts  12237  fsumrelem  12238  binomlem  12250  isumshft  12257  isumsplit  12258  arisum  12265  arisum2  12266  trireciplem  12267  geolim2  12279  geo2sum  12281  0.999...  12288  cvgratz  12299  mertensabs  12304  clim2prod  12306  prodf1f  12310  prodmodclem2a  12343  zproddc  12346  iprodap  12347  iprodap0  12349  fprodseq  12350  prod1dc  12353  prodssdc  12356  fprod2dlemstep  12389  fprodcom2fi  12393  fproddivap  12397  ef0lem  12427  efval2  12432  ege2le3  12438  efaddlem  12441  efsub  12448  eftlub  12457  efsep  12458  tanval3ap  12481  efi4p  12484  sinneg  12493  sinmul  12511  sincossq  12515  cos2t  12517  demoivreALT  12541  eirraplem  12544  dvdsmodexp  12562  odd2np1  12640  omoe  12663  divalglemex  12689  divalglemeuneg  12690  divalgmod  12694  flodddiv4  12703  bitsp1  12718  bitsinv1lem  12728  bitsinv1  12729  gcdneg  12759  gcdaddm  12761  modgcd  12768  bezoutlemnewy  12773  gcdass  12792  gcdmultiple  12797  nninfctlemfo  12817  algrp1  12824  lcmneg  12852  lcmgcdeq  12861  lcmass  12863  cncongr2  12882  prmexpb  12929  sqrt2irr  12940  2sqpwodd  12954  qnumdenbi  12970  phiprmpw  13000  eulerthlema  13008  fermltl  13012  prmdiveq  13014  modprm0  13033  pythagtriplem1  13044  pythagtriplem12  13054  pythagtriplem14  13056  pythagtriplem15  13057  pythagtriplem16  13058  pythagtriplem17  13059  pythagtriplem19  13061  pcpremul  13072  pcneg  13104  pcgcd  13108  pc2dvds  13109  pcaddlem  13118  pcprod  13125  fldivp1  13127  pcbc  13130  prmpwdvds  13134  pockthlem  13135  mul4sqlem  13172  4sqlem11  13180  4sqlem12  13181  4sqlem17  13186  ballotfilemrv  13263  ballotfilemfg  13269  ballotfilemfrc  13270  ballotfilemrinv0  13276  ctiunctlemfo  13330  ressval3d  13426  resseqnbasd  13427  imasival  13627  qusval  13644  plusfeqg  13684  sgrp1  13726  idmhm  13776  resmhm2  13795  mhmeql  13799  grppropstrg  13824  grpinvinv  13872  grp1  13911  imasgrp2  13913  mulgnngzsum  13930  mulginvcom  13950  mulgnndir  13954  mulgdir  13957  mulgneg2  13959  mulgnnass  13960  mulgass  13962  mulgsubdir  13965  trivsubgd  14003  nmzsubg  14013  qussub  14040  idghm  14062  ablinvadd  14114  ablsub2inv  14115  eqgabl  14134  gzsumgsum  14155  gsump1  14157  gsumconstcmn  14166  prdsval  14173  mgpplusgg  14221  mgpbasg  14224  mgpscag  14226  mgptsetg  14227  mgpdsg  14229  mgpress  14230  srgpcomp  14294  srgpcompp  14295  ringo2times  14333  ring1eq0  14353  ring1  14364  opprmulfvalg  14375  crngoppr  14377  opprsllem  14379  oppr1g  14388  opprunitd  14417  rdivmuldivd  14451  rhmunitinv  14485  scafeqg  14645  lmodvsubval2  14679  lmodsubdi  14681  rmodislmod  14688  sralemg  14775  sraipg  14781  crng2idl  14868  cnfldmulg  14913  cnfldexp  14914  cnfldui  14924  mulgrhm2  14945  zrhrhmb  14957  zlmvscag  14968  znval2  14973  znbaslemnn  14974  znunit  14994  psrval  15050  psrgrp  15076  psrneg  15078  mplval2g  15086  restuni2  15278  lmfval  15294  cnfval  15295  cnpfval  15296  txtopon  15363  txcnp  15372  upxp  15373  txrest  15377  cnmptcom  15399  bl2in  15504  xblss2  15506  isxms2  15553  setsmsdsg  15581  setsmstsetg  15582  metss  15595  resubmet  15657  expcn  15670  cncfcncntop  15694  dvidlemap  15792  dvidrelem  15793  dvidsslem  15794  dvcnp2cntop  15800  dvcoapbr  15808  dvcjbr  15809  dvexp  15812  dvexp2  15813  dvrecap  15814  plyaddlem1  15848  plymullem1  15849  plycolemc  15859  plycjlemc  15861  dvply1  15866  efimpi  15920  tangtx  15939  logdivlti  15982  logfac  15995  cxpexprp  15997  rpcxpsub  16010  rpabscxpbnd  16042  rprelogbdiv  16059  binom4  16081  log2tlbndlog2  16082  birthdaylem2  16088  pellexlem2  16092  mpodvdsmulf1o  16104  0sgmppw  16107  lgslem1  16119  lgsmod  16145  lgsdilem  16146  lgsdi  16156  lgsne0  16157  lgsdirnn0  16166  lgsdinn0  16167  lgseisenlem2  16190  lgseisenlem3  16191  lgsquadlem2  16197  lgsquadlem3  16198  lgsquad2lem1  16200  lgsquad3  16203  2lgslem3  16220  2lgsoddprmlem2  16225  2sqlem4  16237  basvtxval2dom  16275  edgfiedgval2dom  16276  setsvtx  16292  ushgredgedgloop  16469  usgr1vr  16489  wlkres  16620  clwwlkccatlem  16641  trlsegvdegfi  16708  eupth2lem3lem2fi  16710  eupth2lem3lem6fi  16712  eupth2lem3lem4fi  16714  depindlem3  16749  bj-charfundcALT  16835  pw1ndom3lem  17019  pw1ndom3  17020  sssneq  17032  0nninf  17047  nnnninfex  17065  nninfnfiinf  17066  repiecele0  17075  trilpolemisumle  17087  qdiff  17098