Theorem eqtr4di 2280

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

Syntax hints:   -> wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  3eqtr4g  2287  rabxmdc  3523  ifpprsnssdc  3774  relop  4872  csbcnvg  4906  dfiun3g  4981  dfiin3g  4982  resima2  5039  relcnvfld  5262  uniabio  5289  fntpg  5377  dffn5im  5681  dfimafn2  5685  fncnvima2  5758  fmptcof  5804  fcoconst  5808  fnasrng  5817  funopsn  5819  fncofn  5821  ffnov  6114  fnovim  6119  fnrnov  6157  foov  6158  funimassov  6161  ovelimab  6162  ofc12  6248  caofinvl  6250  dftpos3  6414  tfr0dm  6474  rdgisucinc  6537  oasuc  6618  ecinxp  6765  phplem1  7021  exmidpw  7081  exmidpweq  7082  unfiin  7099  fidcenumlemr  7133  0ct  7285  ctmlemr  7286  exmidaclem  7401  pw1m  7420  indpi  7540  nqnq0pi  7636  nq0m0r  7654  addnqpr1  7760  recexgt0sr  7971  suplocsrlempr  8005  recidpipr  8054  recidpirq  8056  axrnegex  8077  nntopi  8092  cnref1o  9858  fztp  10286  fseq1m1p1  10303  fz0to4untppr  10332  frecuzrdgrrn  10642  frecuzrdgsuc  10648  frecuzrdgsuctlem  10657  seq3val  10694  seqvalcd  10695  fser0const  10769  mulexpzap  10813  expaddzap  10817  bcp1m1  10999  hash2en  11078  iswrdiz  11091  pfxccatin12lem2c  11278  cjexp  11420  rexuz3  11517  bdtri  11767  climconst  11817  sumfct  11901  zsumdc  11911  fsum3  11914  sum0  11915  fsumcnv  11964  mertenslem2  12063  zproddc  12106  fprodseq  12110  prod0  12112  prod1dc  12113  prodfct  12114  fprodcnv  12152  ef0lem  12187  efzval  12210  efival  12259  sinbnd  12279  cosbnd  12280  eucalgval  12592  eucalginv  12594  eucalglt  12595  eucalgcvga  12596  eucalg  12597  sqpweven  12713  2sqpwodd  12714  dfphi2  12758  phimullem  12763  prmdiv  12773  odzval  12780  pcval  12835  pczpre  12836  pcrec  12847  4sqlem17  12946  ennnfonelemhdmp1  12996  ennnfonelemkh  12999  ressinbasd  13123  restid2  13297  topnvalg  13300  prdsval  13322  prdsbas3  13336  pwsval  13340  pwsbas  13341  pwselbasb  13342  pwsplusgval  13344  pwsmulrval  13345  imasival  13355  imasplusg  13357  qusval  13372  xpsval  13401  ismgm  13406  plusffvalg  13411  grpidvalg  13422  igsumvalx  13438  issgrp  13452  ismnddef  13467  pws0g  13500  ismhm  13510  isgrp  13555  grpn0  13584  grpinvfvalg  13591  grpsubfvalg  13594  pwsinvg  13661  mulgfvalg  13674  mulgval  13675  mulgnn0p1  13686  issubg  13726  isnsg  13755  eqgfval  13775  quseccl0g  13784  isghm  13796  conjsubg  13830  conjsubgen  13831  iscmn  13846  mgpvalg  13902  isrng  13913  issrg  13944  isring  13979  iscrng  13982  opprvalg  14048  dfrhm2  14134  isnzr  14161  islring  14172  issubrg  14201  rrgval  14242  isdomn  14249  islmod  14271  scaffvalg  14286  lsssetm  14336  lspfval  14368  2idlval  14482  2idlvalg  14483  mulgrhm2  14590  zlmval  14607  znval  14616  znzrhfo  14628  znle2  14632  psrval  14646  mplvalcoe  14670  istps  14722  cldval  14789  ntrfval  14790  clsfval  14791  neifval  14830  restbasg  14858  tgrest  14859  txval  14945  upxp  14962  uptx  14964  txrest  14966  lmcn2  14970  cnmpt2t  14983  cnmpt2res  14987  imasnopn  14989  psmetxrge0  15022  xmetge0  15055  isxms  15141  isms  15143  bdxmet  15191  qtopbasss  15211  cnblcld  15225  mpomulcn  15256  negfcncf  15296  dvfvalap  15371  eldvap  15372  dvidlemap  15381  dvidrelem  15382  dvidsslem  15383  dvexp2  15402  dvrecap  15403  dveflem  15416  plyconst  15435  plycolemc  15448  sin0pilem1  15471  ptolemy  15514  coskpi  15538  logbrec  15650  mpodvdsmulf1o  15680  fsumdvdsmul  15681  lgslem1  15695  lgsval  15699  lgsval4  15715  lgsfcl3  15716  lgsdilem  15722  lgsdir2lem4  15726  lgsdir2lem5  15727  gausslemma2dlem5  15761  lgsquadlem2  15773  iedgedgg  15877  isuhgrm  15887  isushgrm  15888  isupgren  15911  isumgren  15921  isuspgren  15971  isusgren  15972  usgrstrrepeen  16045  vtxdgfval  16048  wksfval  16068  ifpsnprss  16089  clwwlkg  16136  clwwlkn1  16160  nninfsellemqall  16469