Theorem eqtr4di 2282

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 2235	. 2 |- B = C
4	1, 3	eqtrdi 2280	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  3eqtr4g  2289  rabxmdc  3528  ifpprsnssdc  3783  relop  4886  csbcnvg  4920  dfiun3g  4995  dfiin3g  4996  resima2  5053  relcnvfld  5277  uniabio  5304  fntpg  5393  dffn5im  5700  dfimafn2  5704  fncnvima2  5777  fmptcof  5822  fcoconst  5826  fnasrng  5836  funopsn  5838  fncofn  5840  ffnov  6135  fnovim  6140  fnrnov  6178  foov  6179  funimassov  6182  ovelimab  6183  ofc12  6268  caofinvl  6270  dftpos3  6471  tfr0dm  6531  rdgisucinc  6594  oasuc  6675  ecinxp  6822  phplem1  7081  exmidpw  7143  exmidpweq  7144  unfiin  7161  fidcenumlemr  7197  0ct  7366  ctmlemr  7367  exmidaclem  7483  pw1m  7502  indpi  7622  nqnq0pi  7718  nq0m0r  7736  addnqpr1  7842  recexgt0sr  8053  suplocsrlempr  8087  recidpipr  8136  recidpirq  8138  axrnegex  8159  nntopi  8174  fcdmnn0supp  9513  fcdmnn0suppg  9514  cnref1o  9946  fztp  10375  fseq1m1p1  10392  fz0to4untppr  10421  frecuzrdgrrn  10733  frecuzrdgsuc  10739  frecuzrdgsuctlem  10748  seq3val  10785  seqvalcd  10786  fser0const  10860  mulexpzap  10904  expaddzap  10908  bcp1m1  11090  hash2en  11170  iswrdiz  11186  pfxccatin12lem2c  11377  cjexp  11533  rexuz3  11630  bdtri  11880  climconst  11930  sumfct  12014  zsumdc  12025  fsum3  12028  sum0  12029  fsumcnv  12078  mertenslem2  12177  zproddc  12220  fprodseq  12224  prod0  12226  prod1dc  12227  prodfct  12228  fprodcnv  12266  ef0lem  12301  efzval  12324  efival  12373  sinbnd  12393  cosbnd  12394  eucalgval  12706  eucalginv  12708  eucalglt  12709  eucalgcvga  12710  eucalg  12711  sqpweven  12827  2sqpwodd  12828  dfphi2  12872  phimullem  12877  prmdiv  12887  odzval  12894  pcval  12949  pczpre  12950  pcrec  12961  4sqlem17  13060  ennnfonelemhdmp1  13110  ennnfonelemkh  13113  ressinbasd  13237  restid2  13411  topnvalg  13414  prdsval  13436  prdsbas3  13450  pwsval  13454  pwsbas  13455  pwselbasb  13456  pwsplusgval  13458  pwsmulrval  13459  imasival  13469  imasplusg  13471  qusval  13486  xpsval  13515  ismgm  13520  plusffvalg  13525  grpidvalg  13536  igsumvalx  13552  issgrp  13566  ismnddef  13581  pws0g  13614  ismhm  13624  isgrp  13669  grpn0  13698  grpinvfvalg  13705  grpsubfvalg  13708  pwsinvg  13775  mulgfvalg  13788  mulgval  13789  mulgnn0p1  13800  issubg  13840  isnsg  13869  eqgfval  13889  quseccl0g  13898  isghm  13910  conjsubg  13944  conjsubgen  13945  iscmn  13960  mgpvalg  14017  isrng  14028  issrg  14059  isring  14094  iscrng  14097  opprvalg  14163  dfrhm2  14249  isnzr  14276  islring  14287  issubrg  14316  rrgval  14357  isdomn  14365  islmod  14387  scaffvalg  14402  lsssetm  14452  lspfval  14484  2idlval  14598  2idlvalg  14599  mulgrhm2  14706  zlmval  14723  znval  14732  znzrhfo  14744  znle2  14748  psrval  14762  mplvalcoe  14791  istps  14843  cldval  14910  ntrfval  14911  clsfval  14912  neifval  14951  restbasg  14979  tgrest  14980  txval  15066  upxp  15083  uptx  15085  txrest  15087  lmcn2  15091  cnmpt2t  15104  cnmpt2res  15108  imasnopn  15110  psmetxrge0  15143  xmetge0  15176  isxms  15262  isms  15264  bdxmet  15312  qtopbasss  15332  cnblcld  15346  mpomulcn  15377  negfcncf  15417  dvfvalap  15492  eldvap  15493  dvidlemap  15502  dvidrelem  15503  dvidsslem  15504  dvexp2  15523  dvrecap  15524  dveflem  15537  plyconst  15556  plycolemc  15569  sin0pilem1  15592  ptolemy  15635  coskpi  15659  logbrec  15771  mpodvdsmulf1o  15804  fsumdvdsmul  15805  lgslem1  15819  lgsval  15823  lgsval4  15839  lgsfcl3  15840  lgsdilem  15846  lgsdir2lem4  15850  lgsdir2lem5  15851  gausslemma2dlem5  15885  lgsquadlem2  15897  iedgedgg  16002  isuhgrm  16012  isushgrm  16013  isupgren  16036  isumgren  16046  isuspgren  16098  isusgren  16099  usgrstrrepeen  16172  vtxdgfval  16229  wksfval  16263  ifpsnprss  16284  clwwlkg  16334  clwwlkn1  16359  eupthsg  16386  eupth2fi  16420  nninfsellemqall  16741  qdiff  16781  gfsumcl  16816