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 )

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:  3eqtr4g  2296  rabxmdc  3554  ifpprsnssdc  3820  relop  4932  csbcnvg  4966  dfiun3g  5041  dfiin3g  5042  resima2  5099  relcnvfld  5324  uniabio  5351  fntpg  5440  dffn5im  5751  dfimafn2  5755  fncnvima2  5833  fmptcof  5878  fcoconst  5882  fnasrng  5892  funopsn  5894  fncofn  5896  ffnov  6195  fnovim  6200  fnrnov  6238  foov  6239  funimassov  6242  ovelimab  6243  ofc12  6330  caofinvl  6332  dftpos3  6537  tfr0dm  6597  rdgisucinc  6660  oasuc  6741  ecinxp  6888  mapunen  7155  phplem1  7157  exmidpw  7219  exmidpweq  7220  unfiin  7237  fidcenumlemr  7277  0ct  7453  ctmlemr  7454  exmidaclem  7570  pw1m  7589  indpi  7715  nqnq0pi  7811  nq0m0r  7829  addnqpr1  7935  recexgt0sr  8146  suplocsrlempr  8180  recidpipr  8229  recidpirq  8231  axrnegex  8252  nntopi  8267  fcdmnn0supp  9626  fcdmnn0suppg  9628  cnref1o  10068  fztp  10502  fseq1m1p1  10519  fz0to4untppr  10548  frecuzrdgrrn  10866  frecuzrdgsuc  10872  frecuzrdgsuctlem  10881  seq3val  10918  seqvalcd  10919  fser0const  10993  mulexpzap  11037  expaddzap  11041  bcp1m1  11225  hashfibclem  11304  hash2en  11317  iswrdiz  11333  pfxccatin12lem2c  11524  cjexp  11680  rexuz3  11778  bdtri  12031  climconst  12081  sumfct  12165  zsumdc  12176  fsum3  12179  sum0  12180  fsumcnv  12229  mertenslem2  12328  zproddc  12371  fprodseq  12375  prod0  12377  prod1dc  12378  prodfct  12379  fprodcnv  12417  ef0lem  12452  efzval  12475  efival  12524  sinbnd  12544  cosbnd  12545  eucalgval  12857  eucalginv  12859  eucalglt  12860  eucalgcvga  12861  eucalg  12862  sqpweven  12980  2sqpwodd  12981  dfphi2  13027  phimullem  13032  prmdiv  13042  odzval  13049  pcval  13104  pczpre  13105  pcrec  13116  4sqlem17  13215  ballotfilemimin  13307  ennnfonelemhdmp1  13358  ennnfonelemkh  13361  ressinbasd  13487  restid2  13661  topnvalg  13664  imasival  13686  imasplusg  13688  qusval  13703  ismgm  13736  plusffvalg  13741  grpidvalg  13752  gzsumvalx  13768  issgrp  13777  ismnddef  13790  ismhm  13827  isgrp  13870  grpn0  13899  grpinvfvalg  13906  grpsubfvalg  13909  mulgfvalg  13983  mulgval  13984  mulgnn0p1  13995  issubg  14035  isnsg  14064  eqgfval  14084  quseccl0g  14093  isghm  14105  conjsubg  14139  conjsubgen  14140  cntrval  14151  cntzfval  14152  iscmn  14186  gsumclfi  14249  gsumf1ofi  14250  gsummptfidmadd  14251  gsum2dfilem2  14272  gsum2dfi  14273  gsumcom2fi  14275  prdsval  14280  prdsbas3  14294  xpsval  14308  pwsval  14311  pwsbas  14312  pwselbasb  14313  pwsplusgval  14315  pwsmulrval  14316  pws0g  14320  pwsinvg  14322  mgpvalg  14327  isrng  14340  issrg  14376  isring  14411  iscrng  14414  opprvalg  14483  dfrhm2  14570  isnzr  14597  islring  14608  issubrg  14638  rrgval  14679  isdomn  14687  isdrngtap  14715  islmod  14736  scaffvalg  14752  lsssetm  14802  lspfval  14834  2idlval  14948  2idlvalg  14949  mulgrhm2  15054  zlmval  15071  znval  15080  znzrhfo  15092  znle2  15096  aspval  15124  asclfval  15130  psrval  15159  mplvalcoe  15206  istps  15258  cldval  15325  ntrfval  15326  clsfval  15327  neifval  15366  restbasg  15394  tgrest  15395  txval  15481  upxp  15498  uptx  15500  txrest  15502  lmcn2  15506  cnmpt2t  15519  cnmpt2res  15523  imasnopn  15525  psmetxrge0  15558  xmetge0  15591  isxms  15677  isms  15679  bdxmet  15727  qtopbasss  15747  cnblcld  15761  mpomulcn  15792  negfcncf  15832  dvfvalap  15907  eldvap  15908  dvidlemap  15917  dvidrelem  15918  dvidsslem  15919  dvexp2  15938  dvrecap  15939  dveflem  15952  plyconst  15971  plycolemc  15984  sin0pilem1  16008  ptolemy  16051  coskpi  16075  logbrec  16196  zprmlogbaplem3  16217  birthdaylem2  16226  prmorcht  16282  mpodvdsmulf1o  16284  fsumdvdsmul  16285  ppiqub  16293  bposlem8  16318  lgslem1  16324  lgsval  16328  lgsval4  16344  lgsfcl3  16345  lgsdilem  16351  lgsdir2lem4  16355  lgsdir2lem5  16356  gausslemma2dlem5  16390  lgsquadlem2  16402  iedgedgg  16507  isuhgrm  16517  isushgrm  16518  isupgren  16541  isumgren  16551  isuspgren  16603  isusgren  16604  usgrstrrepeen  16677  vtxdgfval  16734  wksfval  16768  ifpsnprss  16789  clwwlkg  16839  clwwlkn1  16864  eupthsg  16891  eupth2fi  16925  nninfsellemqall  17264  qdiff  17305