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  6538  tfr0dm  6598  rdgisucinc  6661  oasuc  6742  ecinxp  6889  mapunen  7157  phplem1  7159  exmidpw  7221  exmidpweq  7222  unfiin  7239  fidcenumlemr  7279  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  9627  cnref1o  10067  fztp  10501  fseq1m1p1  10518  fz0to4untppr  10547  frecuzrdgrrn  10865  frecuzrdgsuc  10871  frecuzrdgsuctlem  10880  seq3val  10917  seqvalcd  10918  fser0const  10992  mulexpzap  11036  expaddzap  11040  bcp1m1  11224  hashfibclem  11303  hash2en  11316  iswrdiz  11332  pfxccatin12lem2c  11523  cjexp  11679  rexuz3  11777  bdtri  12030  climconst  12080  sumfct  12164  zsumdc  12175  fsum3  12178  sum0  12179  fsumcnv  12228  mertenslem2  12327  zproddc  12370  fprodseq  12374  prod0  12376  prod1dc  12377  prodfct  12378  fprodcnv  12416  ef0lem  12451  efzval  12474  efival  12523  sinbnd  12543  cosbnd  12544  eucalgval  12856  eucalginv  12858  eucalglt  12859  eucalgcvga  12860  eucalg  12861  sqpweven  12979  2sqpwodd  12980  dfphi2  13026  phimullem  13031  prmdiv  13041  odzval  13048  pcval  13103  pczpre  13104  pcrec  13115  4sqlem17  13214  ballotfilemimin  13306  ennnfonelemhdmp1  13357  ennnfonelemkh  13360  ressinbasd  13486  restid2  13660  topnvalg  13663  imasival  13685  imasplusg  13687  qusval  13702  ismgm  13735  plusffvalg  13740  grpidvalg  13751  gzsumvalx  13767  issgrp  13776  ismnddef  13789  ismhm  13826  isgrp  13869  grpn0  13898  grpinvfvalg  13905  grpsubfvalg  13908  mulgfvalg  13982  mulgval  13983  mulgnn0p1  13994  issubg  14034  isnsg  14063  eqgfval  14083  quseccl0g  14092  isghm  14104  conjsubg  14138  conjsubgen  14139  cntrval  14150  cntzfval  14151  iscmn  14185  gsumclfi  14248  gsumf1ofi  14249  gsummptfidmadd  14250  gsum2dfilem2  14271  gsum2dfi  14272  gsumcom2fi  14274  prdsval  14279  prdsbas3  14293  xpsval  14307  pwsval  14310  pwsbas  14311  pwselbasb  14312  pwsplusgval  14314  pwsmulrval  14315  pws0g  14319  pwsinvg  14321  mgpvalg  14326  isrng  14339  issrg  14375  isring  14410  iscrng  14413  opprvalg  14482  dfrhm2  14569  isnzr  14596  islring  14607  issubrg  14637  rrgval  14678  isdomn  14686  isdrngtap  14714  islmod  14735  scaffvalg  14751  lsssetm  14801  lspfval  14833  2idlval  14947  2idlvalg  14948  mulgrhm2  15053  zlmval  15070  znval  15079  znzrhfo  15091  znle2  15095  aspval  15123  asclfval  15129  psrval  15160  mvrfval  15214  mplvalg  15222  istps  15275  cldval  15342  ntrfval  15343  clsfval  15344  neifval  15383  restbasg  15411  tgrest  15412  txval  15498  upxp  15515  uptx  15517  txrest  15519  lmcn2  15523  cnmpt2t  15536  cnmpt2res  15540  imasnopn  15542  psmetxrge0  15575  xmetge0  15608  isxms  15694  isms  15696  bdxmet  15744  qtopbasss  15764  cnblcld  15778  mpomulcn  15809  negfcncf  15849  dvfvalap  15924  eldvap  15925  dvidlemap  15934  dvidrelem  15935  dvidsslem  15936  dvexp2  15955  dvrecap  15956  dveflem  15969  plyconst  15988  plycolemc  16001  sin0pilem1  16025  ptolemy  16068  coskpi  16092  logbrec  16213  zprmlogbaplem3  16234  birthdaylem2  16243  prmorcht  16299  mpodvdsmulf1o  16301  fsumdvdsmul  16302  ppiqub  16310  bposlem8  16335  lgslem1  16341  lgsval  16345  lgsval4  16361  lgsfcl3  16362  lgsdilem  16368  lgsdir2lem4  16372  lgsdir2lem5  16373  gausslemma2dlem5  16407  lgsquadlem2  16419  iedgedgg  16524  isuhgrm  16534  isushgrm  16535  isupgren  16558  isumgren  16568  isuspgren  16620  isusgren  16621  usgrstrrepeen  16694  vtxdgfval  16751  wksfval  16785  ifpsnprss  16806  clwwlkg  16856  clwwlkn1  16881  eupthsg  16908  eupth2fi  16942  nninfsellemqall  17281  qdiff  17322