Theorem eqtr4d 2213

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

Syntax hints:   -> wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  3eqtr2d  2216  3eqtr2rd  2217  3eqtr4d  2220  3eqtr4rd  2221  3eqtr4a  2236  sbnfc2  3118  ifsbdc  3547  ifeq1dadc  3565  ifeq2dadc  3566  eqifdc  3570  ifnotdc  3572  ifandc  3573  ifordc  3574  onsucuni2  4564  relop  4778  riinint  4889  iotauni  5191  fniinfv  5575  fsn2  5691  fmptapd  5708  fconst2g  5732  fniunfv  5763  ofres  6097  ofco  6101  frecsuclem  6407  frecrdg  6409  oasuc  6465  nnacom  6485  nnaass  6486  nndi  6487  nnmass  6488  nnmsucr  6489  nnmcom  6490  funresdfunsndc  6507  uniqs2  6595  en1bg  6800  fundmen  6806  1domsn  6819  mapxpen  6848  xpmapenlem  6849  phplem4dom  6862  en2eqpr  6907  sbthlemi5  6960  omp1eomlem  7093  difinfsnlem  7098  ctmlemr  7107  ctssdccl  7110  ctssdc  7112  infnninf  7122  infnninfOLD  7123  nnnninfeq  7126  exmidonfinlem  7192  exmidmotap  7260  addcmpblnq  7366  distrnqg  7386  ltexnqq  7407  addcmpblnq0  7442  nqnq0a  7453  nqnq0m  7454  nq0m0r  7455  nq0a0  7456  nnanq0  7457  distrnq0  7458  prarloclemlo  7493  prarloclemcalc  7501  genpassl  7523  genpassu  7524  ltsosr  7763  0idsr  7766  1idsr  7767  mulextsr1lem  7779  cnegex  8135  subsub3  8189  subadd4  8201  mulneg12  8354  mulsub  8358  apreap  8544  cru  8559  recextlem1  8608  cju  8918  halfaddsub  9153  nn0supp  9228  nneo  9356  zeo2  9359  uzin  9560  xaddcom  9861  xaddass  9869  xleaddadd  9887  iccf1o  10004  fzsuc2  10079  flqeqceilz  10318  zmod1congr  10341  modqcyc  10359  modqcyc2  10360  modqaddabs  10362  modqmul1  10377  modqaddmulmod  10391  addmodlteq  10398  frec2uzrdg  10409  frecuzrdgsuctlem  10423  seq3val  10458  seqvalcd  10459  seq3fveq2  10469  seq3split  10479  seq3distr  10513  ser0f  10515  expp1  10527  mulexp  10559  mulexpzap  10560  expadd  10562  expaddzap  10564  expmul  10565  expmulzap  10566  expsubap  10568  expdivap  10571  subsq  10627  mulbinom2  10637  binom3  10638  bernneq  10641  modqexp  10647  nn0opthd  10702  faclbnd  10721  faclbnd6  10724  bccmpl  10734  bcp1n  10741  zfz1isolemiso  10819  seq3coll  10822  shftval2  10835  shftval4  10837  seq3shft  10847  crre  10866  remim  10869  remullem  10880  cjexp  10902  cnrecnv  10919  resqrexlemlo  11022  resqrexlemcalc1  11023  resqrexlemcalc2  11024  resqrexlemcalc3  11025  resqrexlemnm  11027  rsqrmo  11036  abscj  11061  absid  11080  absre  11086  recvalap  11106  maxabsle  11213  maxltsup  11227  2zsupmax  11234  minabs  11244  bdtrilem  11247  bdtri  11248  2zinfmin  11251  xrmaxiflemab  11255  xrmaxiflemcom  11257  xrmaxadd  11269  xrbdtri  11284  iooinsup  11285  climaddc1  11337  climmulc2  11339  climsubc1  11340  climsubc2  11341  climcvg1nlem  11357  summodclem3  11388  zsumdc  11392  isum  11393  isumz  11397  isumss  11399  fisumss  11400  fsum3cvg2  11402  fsumadd  11414  isummulc2  11434  sumsplitdc  11440  fsum2dlemstep  11442  fisumcom2  11446  fisum0diag2  11455  fsumconst  11462  telfsumo  11474  fsumparts  11478  fsumrelem  11479  binomlem  11491  isumshft  11498  isumsplit  11499  arisum  11506  arisum2  11507  trireciplem  11508  geolim2  11520  geo2sum  11522  0.999...  11529  cvgratz  11540  mertensabs  11545  clim2prod  11547  prodf1f  11551  prodmodclem2a  11584  zproddc  11587  iprodap  11588  iprodap0  11590  fprodseq  11591  prod1dc  11594  prodssdc  11597  fprod2dlemstep  11630  fprodcom2fi  11634  fproddivap  11638  ef0lem  11668  efval2  11673  ege2le3  11679  efaddlem  11682  efsub  11689  eftlub  11698  efsep  11699  tanval3ap  11722  efi4p  11725  sinneg  11734  sinmul  11752  sincossq  11756  cos2t  11758  demoivreALT  11781  eirraplem  11784  dvdsmodexp  11802  odd2np1  11878  omoe  11901  divalglemex  11927  divalglemeuneg  11928  divalgmod  11932  flodddiv4  11939  gcdneg  11983  gcdaddm  11985  modgcd  11992  bezoutlemnewy  11997  gcdass  12016  gcdmultiple  12021  algrp1  12046  lcmneg  12074  lcmgcdeq  12083  lcmass  12085  cncongr2  12104  prmexpb  12151  sqrt2irr  12162  2sqpwodd  12176  qnumdenbi  12192  phiprmpw  12222  eulerthlema  12230  fermltl  12234  prmdiveq  12236  modprm0  12254  pythagtriplem1  12265  pythagtriplem12  12275  pythagtriplem14  12277  pythagtriplem15  12278  pythagtriplem16  12279  pythagtriplem17  12280  pythagtriplem19  12282  pcpremul  12293  pcneg  12324  pcgcd  12328  pc2dvds  12329  pcaddlem  12338  pcprod  12344  fldivp1  12346  pcbc  12349  prmpwdvds  12353  pockthlem  12354  mul4sqlem  12391  ctiunctlemfo  12440  strslfv3  12508  ressval3d  12531  resseqnbasd  12532  imasival  12727  qusval  12744  plusfeqg  12783  sgrp1  12816  idmhm  12860  mhmeql  12876  grppropstrg  12895  grpinvinv  12937  grp1  12976  mulginvcom  13008  mulgnndir  13012  mulgdir  13015  mulgneg2  13017  mulgnnass  13018  mulgass  13020  mulgsubdir  13023  trivsubgd  13060  nmzsubg  13070  ablinvadd  13113  ablsub2inv  13114  mgpplusgg  13134  mgpbasg  13136  mgpscag  13137  mgptsetg  13138  mgpdsg  13140  mgpress  13141  srgpcomp  13173  srgpcompp  13174  ringo2times  13211  ring1eq0  13225  ring1  13236  opprmulfvalg  13242  crngoppr  13244  opprsllem  13246  oppr1g  13252  opprunitd  13279  rdivmuldivd  13313  scafeqg  13398  lmodvsubval2  13432  lmodsubdi  13434  rmodislmod  13441  cnfldmulg  13473  cnfldexp  13474  restuni2  13680  lmfval  13695  cnfval  13697  cnpfval  13698  txtopon  13765  txcnp  13774  upxp  13775  txrest  13779  cnmptcom  13801  bl2in  13906  xblss2  13908  isxms2  13955  setsmsdsg  13983  setsmstsetg  13984  metss  13997  resubmet  14051  cncfcncntop  14083  dvidlemap  14163  dvcnp2cntop  14166  dvcoapbr  14174  dvcjbr  14175  dvexp  14178  dvexp2  14179  dvrecap  14180  efimpi  14243  tangtx  14262  logdivlti  14305  cxpexprp  14319  rpcxpsub  14332  rpabscxpbnd  14362  rprelogbdiv  14378  binom4  14400  lgslem1  14404  lgsmod  14430  lgsdilem  14431  lgsdi  14441  lgsne0  14442  lgsdirnn0  14451  lgsdinn0  14452  lgseisenlem2  14454  2lgsoddprmlem2  14457  2sqlem4  14468  bj-charfundcALT  14564  sssneq  14754  0nninf  14756  trilpolemisumle  14789