Theorem eqtr4di 2289

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqtr4di.1	|- ( ph -> A = B )
eqtr4di.2	|- C = B

Assertion

Ref	Expression
eqtr4di	|- ( ph -> A = C )

Proof of Theorem eqtr4di

Step	Hyp	Ref	Expression
1		eqtr4di.1	. 2 |- ( ph -> A = B )
2		eqtr4di.2	. . 3 |- C = B
3	2	eqcomi 2242	. 2 |- B = C
4	1, 3	eqtrdi 2287	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  3eqtr4g  2296  rabxmdc  3554  ifpprsnssdc  3815  relop  4925  csbcnvg  4959  dfiun3g  5034  dfiin3g  5035  resima2  5092  relcnvfld  5316  uniabio  5343  fntpg  5432  dffn5im  5742  dfimafn2  5746  fncnvima2  5821  fmptcof  5866  fcoconst  5870  fnasrng  5880  funopsn  5882  fncofn  5884  ffnov  6182  fnovim  6187  fnrnov  6225  foov  6226  funimassov  6229  ovelimab  6230  ofc12  6316  caofinvl  6318  dftpos3  6523  tfr0dm  6583  rdgisucinc  6646  oasuc  6727  ecinxp  6874  mapunen  7141  phplem1  7143  exmidpw  7205  exmidpweq  7206  unfiin  7223  fidcenumlemr  7262  0ct  7437  ctmlemr  7438  exmidaclem  7554  pw1m  7573  indpi  7699  nqnq0pi  7795  nq0m0r  7813  addnqpr1  7919  recexgt0sr  8130  suplocsrlempr  8164  recidpipr  8213  recidpirq  8215  axrnegex  8236  nntopi  8251  fcdmnn0supp  9594  fcdmnn0suppg  9596  cnref1o  10030  fztp  10463  fseq1m1p1  10480  fz0to4untppr  10509  frecuzrdgrrn  10823  frecuzrdgsuc  10829  frecuzrdgsuctlem  10838  seq3val  10875  seqvalcd  10876  fser0const  10950  mulexpzap  10994  expaddzap  10998  bcp1m1  11181  hashfibclem  11260  hash2en  11273  iswrdiz  11289  pfxccatin12lem2c  11480  cjexp  11636  rexuz3  11734  bdtri  11984  climconst  12034  sumfct  12118  zsumdc  12129  fsum3  12132  sum0  12133  fsumcnv  12182  mertenslem2  12281  zproddc  12324  fprodseq  12328  prod0  12330  prod1dc  12331  prodfct  12332  fprodcnv  12370  ef0lem  12405  efzval  12428  efival  12477  sinbnd  12497  cosbnd  12498  eucalgval  12810  eucalginv  12812  eucalglt  12813  eucalgcvga  12814  eucalg  12815  sqpweven  12931  2sqpwodd  12932  dfphi2  12976  phimullem  12981  prmdiv  12991  odzval  12998  pcval  13053  pczpre  13054  pcrec  13065  4sqlem17  13164  ballotfilemimin  13227  ennnfonelemhdmp1  13278  ennnfonelemkh  13281  ressinbasd  13405  restid2  13579  topnvalg  13582  imasival  13604  imasplusg  13606  qusval  13621  ismgm  13654  plusffvalg  13659  grpidvalg  13670  gzsumvalx  13686  issgrp  13695  ismnddef  13708  ismhm  13745  isgrp  13788  grpn0  13817  grpinvfvalg  13824  grpsubfvalg  13827  mulgfvalg  13901  mulgval  13902  mulgnn0p1  13913  issubg  13953  isnsg  13982  eqgfval  14002  quseccl0g  14011  isghm  14023  conjsubg  14057  conjsubgen  14058  iscmn  14073  gsumclfi  14136  gsumf1ofi  14137  gsummptfidmadd  14138  prdsval  14150  prdsbas3  14164  xpsval  14178  pwsval  14181  pwsbas  14182  pwselbasb  14183  pwsplusgval  14185  pwsmulrval  14186  pws0g  14190  pwsinvg  14192  mgpvalg  14197  isrng  14208  issrg  14243  isring  14278  iscrng  14281  opprvalg  14347  dfrhm2  14434  isnzr  14461  islring  14472  issubrg  14502  rrgval  14543  isdomn  14551  isdrngtap  14579  islmod  14600  scaffvalg  14615  lsssetm  14665  lspfval  14697  2idlval  14811  2idlvalg  14812  mulgrhm2  14917  zlmval  14934  znval  14943  znzrhfo  14955  znle2  14959  psrval  14973  mplvalcoe  15004  istps  15056  cldval  15123  ntrfval  15124  clsfval  15125  neifval  15164  restbasg  15192  tgrest  15193  txval  15279  upxp  15296  uptx  15298  txrest  15300  lmcn2  15304  cnmpt2t  15317  cnmpt2res  15321  imasnopn  15323  psmetxrge0  15356  xmetge0  15389  isxms  15475  isms  15477  bdxmet  15525  qtopbasss  15545  cnblcld  15559  mpomulcn  15590  negfcncf  15630  dvfvalap  15705  eldvap  15706  dvidlemap  15715  dvidrelem  15716  dvidsslem  15717  dvexp2  15736  dvrecap  15737  dveflem  15750  plyconst  15769  plycolemc  15782  sin0pilem1  15805  ptolemy  15848  coskpi  15872  logbrec  15985  mpodvdsmulf1o  16018  fsumdvdsmul  16019  lgslem1  16033  lgsval  16037  lgsval4  16053  lgsfcl3  16054  lgsdilem  16060  lgsdir2lem4  16064  lgsdir2lem5  16065  gausslemma2dlem5  16099  lgsquadlem2  16111  iedgedgg  16216  isuhgrm  16226  isushgrm  16227  isupgren  16250  isumgren  16260  isuspgren  16312  isusgren  16313  usgrstrrepeen  16386  vtxdgfval  16443  wksfval  16477  ifpsnprss  16498  clwwlkg  16548  clwwlkn1  16573  eupthsg  16600  eupth2fi  16634  nninfsellemqall  16963  qdiff  17003