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  3117  ifsbdc  3546  ifeq1dadc  3564  eqifdc  3568  ifnotdc  3570  ifandc  3571  ifordc  3572  onsucuni2  4560  relop  4773  riinint  4884  iotauni  5186  fniinfv  5570  fsn2  5686  fmptapd  5703  fconst2g  5727  fniunfv  5757  ofres  6091  ofco  6095  frecsuclem  6401  frecrdg  6403  oasuc  6459  nnacom  6479  nnaass  6480  nndi  6481  nnmass  6482  nnmsucr  6483  nnmcom  6484  funresdfunsndc  6501  uniqs2  6589  en1bg  6794  fundmen  6800  1domsn  6813  mapxpen  6842  xpmapenlem  6843  phplem4dom  6856  en2eqpr  6901  sbthlemi5  6954  omp1eomlem  7087  difinfsnlem  7092  ctmlemr  7101  ctssdccl  7104  ctssdc  7106  infnninf  7116  infnninfOLD  7117  nnnninfeq  7120  exmidonfinlem  7186  exmidmotap  7251  addcmpblnq  7357  distrnqg  7377  ltexnqq  7398  addcmpblnq0  7433  nqnq0a  7444  nqnq0m  7445  nq0m0r  7446  nq0a0  7447  nnanq0  7448  distrnq0  7449  prarloclemlo  7484  prarloclemcalc  7492  genpassl  7514  genpassu  7515  ltsosr  7754  0idsr  7757  1idsr  7758  mulextsr1lem  7770  cnegex  8125  subsub3  8179  subadd4  8191  mulneg12  8344  mulsub  8348  apreap  8534  cru  8549  recextlem1  8597  cju  8907  halfaddsub  9142  nn0supp  9217  nneo  9345  zeo2  9348  uzin  9549  xaddcom  9848  xaddass  9856  xleaddadd  9874  iccf1o  9991  fzsuc2  10065  flqeqceilz  10304  zmod1congr  10327  modqcyc  10345  modqcyc2  10346  modqaddabs  10348  modqmul1  10363  modqaddmulmod  10377  addmodlteq  10384  frec2uzrdg  10395  frecuzrdgsuctlem  10409  seq3val  10444  seqvalcd  10445  seq3fveq2  10455  seq3split  10465  seq3distr  10499  ser0f  10501  expp1  10513  mulexp  10545  mulexpzap  10546  expadd  10548  expaddzap  10550  expmul  10551  expmulzap  10552  expsubap  10554  expdivap  10557  subsq  10612  mulbinom2  10622  binom3  10623  bernneq  10626  modqexp  10632  nn0opthd  10686  faclbnd  10705  faclbnd6  10708  bccmpl  10718  bcp1n  10725  zfz1isolemiso  10803  seq3coll  10806  shftval2  10819  shftval4  10821  seq3shft  10831  crre  10850  remim  10853  remullem  10864  cjexp  10886  cnrecnv  10903  resqrexlemlo  11006  resqrexlemcalc1  11007  resqrexlemcalc2  11008  resqrexlemcalc3  11009  resqrexlemnm  11011  rsqrmo  11020  abscj  11045  absid  11064  absre  11070  recvalap  11090  maxabsle  11197  maxltsup  11211  2zsupmax  11218  minabs  11228  bdtrilem  11231  bdtri  11232  2zinfmin  11235  xrmaxiflemab  11239  xrmaxiflemcom  11241  xrmaxadd  11253  xrbdtri  11268  iooinsup  11269  climaddc1  11321  climmulc2  11323  climsubc1  11324  climsubc2  11325  climcvg1nlem  11341  summodclem3  11372  zsumdc  11376  isum  11377  isumz  11381  isumss  11383  fisumss  11384  fsum3cvg2  11386  fsumadd  11398  isummulc2  11418  sumsplitdc  11424  fsum2dlemstep  11426  fisumcom2  11430  fisum0diag2  11439  fsumconst  11446  telfsumo  11458  fsumparts  11462  fsumrelem  11463  binomlem  11475  isumshft  11482  isumsplit  11483  arisum  11490  arisum2  11491  trireciplem  11492  geolim2  11504  geo2sum  11506  0.999...  11513  cvgratz  11524  mertensabs  11529  clim2prod  11531  prodf1f  11535  prodmodclem2a  11568  zproddc  11571  iprodap  11572  iprodap0  11574  fprodseq  11575  prod1dc  11578  prodssdc  11581  fprod2dlemstep  11614  fprodcom2fi  11618  fproddivap  11622  ef0lem  11652  efval2  11657  ege2le3  11663  efaddlem  11666  efsub  11673  eftlub  11682  efsep  11683  tanval3ap  11706  efi4p  11709  sinneg  11718  sinmul  11736  sincossq  11740  cos2t  11742  demoivreALT  11765  eirraplem  11768  dvdsmodexp  11786  odd2np1  11861  omoe  11884  divalglemex  11910  divalglemeuneg  11911  divalgmod  11915  flodddiv4  11922  gcdneg  11966  gcdaddm  11968  modgcd  11975  bezoutlemnewy  11980  gcdass  11999  gcdmultiple  12004  algrp1  12029  lcmneg  12057  lcmgcdeq  12066  lcmass  12068  cncongr2  12087  prmexpb  12134  sqrt2irr  12145  2sqpwodd  12159  qnumdenbi  12175  phiprmpw  12205  eulerthlema  12213  fermltl  12217  prmdiveq  12219  modprm0  12237  pythagtriplem1  12248  pythagtriplem12  12258  pythagtriplem14  12260  pythagtriplem15  12261  pythagtriplem16  12262  pythagtriplem17  12263  pythagtriplem19  12265  pcpremul  12276  pcneg  12307  pcgcd  12311  pc2dvds  12312  pcaddlem  12321  pcprod  12327  fldivp1  12329  pcbc  12332  prmpwdvds  12336  pockthlem  12337  mul4sqlem  12374  ctiunctlemfo  12423  strslfv3  12490  ressval3d  12513  resseqnbasd  12514  plusfeqg  12675  sgrp1  12708  idmhm  12750  mhmeql  12766  grppropstrg  12785  grpinvinv  12826  grp1  12865  mulginvcom  12896  mulgnndir  12900  mulgdir  12903  mulgneg2  12905  mulgnnass  12906  mulgass  12908  mulgsubdir  12911  ablinvadd  12940  ablsub2inv  12941  mgpplusgg  12961  mgpbasg  12963  mgpscag  12964  mgptsetg  12965  mgpdsg  12967  srgpcomp  12999  srgpcompp  13000  rngo2times  13037  ring1eq0  13051  ring1  13062  opprmulfvalg  13067  crngoppr  13069  opprsllem  13071  oppr1g  13077  opprunitd  13104  restuni2  13344  lmfval  13359  cnfval  13361  cnpfval  13362  txtopon  13429  txcnp  13438  upxp  13439  txrest  13443  cnmptcom  13465  bl2in  13570  xblss2  13572  isxms2  13619  setsmsdsg  13647  setsmstsetg  13648  metss  13661  resubmet  13715  cncfcncntop  13747  dvidlemap  13827  dvcnp2cntop  13830  dvcoapbr  13838  dvcjbr  13839  dvexp  13842  dvexp2  13843  dvrecap  13844  efimpi  13907  tangtx  13926  logdivlti  13969  cxpexprp  13983  rpcxpsub  13996  rpabscxpbnd  14026  rprelogbdiv  14042  binom4  14064  lgslem1  14068  lgsmod  14094  lgsdilem  14095  lgsdi  14105  lgsne0  14106  lgsdirnn0  14115  lgsdinn0  14116  2sqlem4  14121  bj-charfundcALT  14217  sssneq  14407  0nninf  14409  trilpolemisumle  14442