Theorem eqtr4d 2241

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

Syntax hints:   -> wi 4   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  3eqtr2d  2244  3eqtr2rd  2245  3eqtr4d  2248  3eqtr4rd  2249  3eqtr4a  2264  sbnfc2  3154  ifsbdc  3583  ifeq1dadc  3601  ifeq2dadc  3602  eqifdc  3607  ifnotdc  3609  ifandc  3610  ifordc  3611  onsucuni2  4613  relop  4829  riinint  4940  iotauni  5245  fniinfv  5639  fsn2  5756  fmptapd  5777  fconst2g  5801  fniunfv  5833  ofres  6175  ofco  6179  caofid1  6189  caofid2  6190  frecsuclem  6494  frecrdg  6496  oasuc  6552  nnacom  6572  nnaass  6573  nndi  6574  nnmass  6575  nnmsucr  6576  nnmcom  6577  funresdfunsndc  6594  uniqs2  6684  en1bg  6894  fundmen  6900  1domsn  6916  pw2f1odclem  6933  mapxpen  6947  xpmapenlem  6948  phplem4dom  6961  en2eqpr  7006  sbthlemi5  7065  omp1eomlem  7198  difinfsnlem  7203  ctmlemr  7212  ctssdccl  7215  ctssdc  7217  infnninf  7228  infnninfOLD  7229  nnnninfeq  7232  exmidonfinlem  7303  exmidmotap  7375  addcmpblnq  7482  distrnqg  7502  ltexnqq  7523  addcmpblnq0  7558  nqnq0a  7569  nqnq0m  7570  nq0m0r  7571  nq0a0  7572  nnanq0  7573  distrnq0  7574  prarloclemlo  7609  prarloclemcalc  7617  genpassl  7639  genpassu  7640  ltsosr  7879  0idsr  7882  1idsr  7883  mulextsr1lem  7895  cnegex  8252  subsub3  8306  subadd4  8318  mulneg12  8471  mulsub  8475  apreap  8662  cru  8677  recextlem1  8726  cju  9036  ofnegsub  9037  halfaddsub  9273  nn0supp  9349  nneo  9478  zeo2  9481  uzin  9683  xaddcom  9985  xaddass  9993  xleaddadd  10011  iccf1o  10128  fzsuc2  10203  fldiv4lem1div2uz2  10451  flqeqceilz  10465  zmod1congr  10488  modqcyc  10506  modqcyc2  10507  modqaddabs  10509  modqmul1  10524  modqaddmulmod  10538  addmodlteq  10545  frec2uzrdg  10556  frecuzrdgsuctlem  10570  seq3val  10607  seqvalcd  10608  seq3fveq2  10622  seqfveq2g  10624  seq3split  10635  seqsplitg  10636  seqf1oglem2a  10665  seqf1oglem2  10667  seqfeq4g  10678  seq3distr  10679  ser0f  10681  expp1  10693  mulexp  10725  mulexpzap  10726  expadd  10728  expaddzap  10730  expmul  10731  expmulzap  10732  expsubap  10734  expdivap  10737  subsq  10793  mulbinom2  10803  binom3  10804  bernneq  10807  modqexp  10813  nn0opthd  10869  faclbnd  10888  faclbnd6  10891  bccmpl  10901  bcp1n  10908  zfz1isolemiso  10986  seq3coll  10989  ccatsymb  11061  ccatval1lsw  11063  ccatass  11067  eqs1  11085  lswccats1fst  11099  swrdsb0eq  11121  swrdsbslen  11122  swrds1  11124  ccatswrd  11126  pfxres  11135  ccatpfx  11155  shftval2  11170  shftval4  11172  seq3shft  11182  crre  11201  remim  11204  remullem  11215  cjexp  11237  cnrecnv  11254  resqrexlemlo  11357  resqrexlemcalc1  11358  resqrexlemcalc2  11359  resqrexlemcalc3  11360  resqrexlemnm  11362  rsqrmo  11371  abscj  11396  absid  11415  absre  11421  recvalap  11441  maxabsle  11548  maxltsup  11562  2zsupmax  11570  minabs  11580  bdtrilem  11583  bdtri  11584  2zinfmin  11587  xrmaxiflemab  11591  xrmaxiflemcom  11593  xrmaxadd  11605  xrbdtri  11620  iooinsup  11621  climaddc1  11673  climmulc2  11675  climsubc1  11676  climsubc2  11677  climcvg1nlem  11693  summodclem3  11724  zsumdc  11728  isum  11729  isumz  11733  isumss  11735  fisumss  11736  fsum3cvg2  11738  fsumadd  11750  isummulc2  11770  sumsplitdc  11776  fsum2dlemstep  11778  fisumcom2  11782  fisum0diag2  11791  fsumconst  11798  telfsumo  11810  fsumparts  11814  fsumrelem  11815  binomlem  11827  isumshft  11834  isumsplit  11835  arisum  11842  arisum2  11843  trireciplem  11844  geolim2  11856  geo2sum  11858  0.999...  11865  cvgratz  11876  mertensabs  11881  clim2prod  11883  prodf1f  11887  prodmodclem2a  11920  zproddc  11923  iprodap  11924  iprodap0  11926  fprodseq  11927  prod1dc  11930  prodssdc  11933  fprod2dlemstep  11966  fprodcom2fi  11970  fproddivap  11974  ef0lem  12004  efval2  12009  ege2le3  12015  efaddlem  12018  efsub  12025  eftlub  12034  efsep  12035  tanval3ap  12058  efi4p  12061  sinneg  12070  sinmul  12088  sincossq  12092  cos2t  12094  demoivreALT  12118  eirraplem  12121  dvdsmodexp  12139  odd2np1  12217  omoe  12240  divalglemex  12266  divalglemeuneg  12267  divalgmod  12271  flodddiv4  12280  bitsp1  12295  bitsinv1lem  12305  bitsinv1  12306  gcdneg  12336  gcdaddm  12338  modgcd  12345  bezoutlemnewy  12350  gcdass  12369  gcdmultiple  12374  nninfctlemfo  12394  algrp1  12401  lcmneg  12429  lcmgcdeq  12438  lcmass  12440  cncongr2  12459  prmexpb  12506  sqrt2irr  12517  2sqpwodd  12531  qnumdenbi  12547  phiprmpw  12577  eulerthlema  12585  fermltl  12589  prmdiveq  12591  modprm0  12610  pythagtriplem1  12621  pythagtriplem12  12631  pythagtriplem14  12633  pythagtriplem15  12634  pythagtriplem16  12635  pythagtriplem17  12636  pythagtriplem19  12638  pcpremul  12649  pcneg  12681  pcgcd  12685  pc2dvds  12686  pcaddlem  12695  pcprod  12702  fldivp1  12704  pcbc  12707  prmpwdvds  12711  pockthlem  12712  mul4sqlem  12749  4sqlem11  12757  4sqlem12  12758  4sqlem17  12763  ctiunctlemfo  12843  ressval3d  12937  resseqnbasd  12938  prdsval  13138  imasival  13171  qusval  13188  plusfeqg  13229  sgrp1  13276  idmhm  13334  resmhm2  13353  mhmeql  13357  grppropstrg  13384  grpinvinv  13432  grp1  13471  imasgrp2  13479  mulgnngsum  13496  mulginvcom  13516  mulgnndir  13520  mulgdir  13523  mulgneg2  13525  mulgnnass  13526  mulgass  13528  mulgsubdir  13531  trivsubgd  13569  nmzsubg  13579  qussub  13606  idghm  13628  ablinvadd  13679  ablsub2inv  13680  eqgabl  13699  mgpplusgg  13719  mgpbasg  13721  mgpscag  13722  mgptsetg  13723  mgpdsg  13725  mgpress  13726  srgpcomp  13785  srgpcompp  13786  ringo2times  13823  ring1eq0  13843  ring1  13854  opprmulfvalg  13865  crngoppr  13867  opprsllem  13869  oppr1g  13877  opprunitd  13905  rdivmuldivd  13939  rhmunitinv  13973  scafeqg  14103  lmodvsubval2  14137  lmodsubdi  14139  rmodislmod  14146  sralemg  14233  sraipg  14239  crng2idl  14326  cnfldmulg  14371  cnfldexp  14372  cnfldui  14384  mulgrhm2  14405  zrhrhmb  14417  zlmvscag  14428  znval2  14433  znbaslemnn  14434  znunit  14454  psrval  14461  psrgrp  14480  psrneg  14482  mplval2g  14490  restuni2  14682  lmfval  14697  cnfval  14699  cnpfval  14700  txtopon  14767  txcnp  14776  upxp  14777  txrest  14781  cnmptcom  14803  bl2in  14908  xblss2  14910  isxms2  14957  setsmsdsg  14985  setsmstsetg  14986  metss  14999  resubmet  15061  expcn  15074  cncfcncntop  15098  dvidlemap  15196  dvidrelem  15197  dvidsslem  15198  dvcnp2cntop  15204  dvcoapbr  15212  dvcjbr  15213  dvexp  15216  dvexp2  15217  dvrecap  15218  plyaddlem1  15252  plymullem1  15253  plycolemc  15263  plycjlemc  15265  dvply1  15270  efimpi  15324  tangtx  15343  logdivlti  15386  cxpexprp  15400  rpcxpsub  15413  rpabscxpbnd  15445  rprelogbdiv  15462  binom4  15484  mpodvdsmulf1o  15495  0sgmppw  15498  lgslem1  15510  lgsmod  15536  lgsdilem  15537  lgsdi  15547  lgsne0  15548  lgsdirnn0  15557  lgsdinn0  15558  lgseisenlem2  15581  lgseisenlem3  15582  lgsquadlem2  15588  lgsquadlem3  15589  lgsquad2lem1  15591  lgsquad3  15594  2lgslem3  15611  2lgsoddprmlem2  15616  2sqlem4  15628  basvtxval2dom  15664  edgfiedgval2dom  15665  bj-charfundcALT  15782  1dom1el  15964  2omap  15969  sssneq  15976  0nninf  15978  nnnninfex  15996  nninfnfiinf  15997  trilpolemisumle  16014