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  5679  dfimafn2  5683  fncnvima2  5756  fmptcof  5802  fcoconst  5806  fnasrng  5815  funopsn  5817  ffnov  6108  fnovim  6113  fnrnov  6151  foov  6152  funimassov  6155  ovelimab  6156  ofc12  6242  caofinvl  6244  dftpos3  6408  tfr0dm  6468  rdgisucinc  6531  oasuc  6610  ecinxp  6757  phplem1  7013  exmidpw  7070  exmidpweq  7071  unfiin  7088  fidcenumlemr  7122  0ct  7274  ctmlemr  7275  exmidaclem  7390  pw1m  7409  indpi  7529  nqnq0pi  7625  nq0m0r  7643  addnqpr1  7749  recexgt0sr  7960  suplocsrlempr  7994  recidpipr  8043  recidpirq  8045  axrnegex  8066  nntopi  8081  cnref1o  9846  fztp  10274  fseq1m1p1  10291  fz0to4untppr  10320  frecuzrdgrrn  10630  frecuzrdgsuc  10636  frecuzrdgsuctlem  10645  seq3val  10682  seqvalcd  10683  fser0const  10757  mulexpzap  10801  expaddzap  10805  bcp1m1  10987  hash2en  11065  iswrdiz  11078  pfxccatin12lem2c  11262  cjexp  11404  rexuz3  11501  bdtri  11751  climconst  11801  sumfct  11885  zsumdc  11895  fsum3  11898  sum0  11899  fsumcnv  11948  mertenslem2  12047  zproddc  12090  fprodseq  12094  prod0  12096  prod1dc  12097  prodfct  12098  fprodcnv  12136  ef0lem  12171  efzval  12194  efival  12243  sinbnd  12263  cosbnd  12264  eucalgval  12576  eucalginv  12578  eucalglt  12579  eucalgcvga  12580  eucalg  12581  sqpweven  12697  2sqpwodd  12698  dfphi2  12742  phimullem  12747  prmdiv  12757  odzval  12764  pcval  12819  pczpre  12820  pcrec  12831  4sqlem17  12930  ennnfonelemhdmp1  12980  ennnfonelemkh  12983  ressinbasd  13107  restid2  13281  topnvalg  13284  prdsval  13306  prdsbas3  13320  pwsval  13324  pwsbas  13325  pwselbasb  13326  pwsplusgval  13328  pwsmulrval  13329  imasival  13339  imasplusg  13341  qusval  13356  xpsval  13385  ismgm  13390  plusffvalg  13395  grpidvalg  13406  igsumvalx  13422  issgrp  13436  ismnddef  13451  pws0g  13484  ismhm  13494  isgrp  13539  grpn0  13568  grpinvfvalg  13575  grpsubfvalg  13578  pwsinvg  13645  mulgfvalg  13658  mulgval  13659  mulgnn0p1  13670  issubg  13710  isnsg  13739  eqgfval  13759  quseccl0g  13768  isghm  13780  conjsubg  13814  conjsubgen  13815  iscmn  13830  mgpvalg  13886  isrng  13897  issrg  13928  isring  13963  iscrng  13966  opprvalg  14032  dfrhm2  14118  isnzr  14145  islring  14156  issubrg  14185  rrgval  14226  isdomn  14233  islmod  14255  scaffvalg  14270  lsssetm  14320  lspfval  14352  2idlval  14466  2idlvalg  14467  mulgrhm2  14574  zlmval  14591  znval  14600  znzrhfo  14612  znle2  14616  psrval  14630  mplvalcoe  14654  istps  14706  cldval  14773  ntrfval  14774  clsfval  14775  neifval  14814  restbasg  14842  tgrest  14843  txval  14929  upxp  14946  uptx  14948  txrest  14950  lmcn2  14954  cnmpt2t  14967  cnmpt2res  14971  imasnopn  14973  psmetxrge0  15006  xmetge0  15039  isxms  15125  isms  15127  bdxmet  15175  qtopbasss  15195  cnblcld  15209  mpomulcn  15240  negfcncf  15280  dvfvalap  15355  eldvap  15356  dvidlemap  15365  dvidrelem  15366  dvidsslem  15367  dvexp2  15386  dvrecap  15387  dveflem  15400  plyconst  15419  plycolemc  15432  sin0pilem1  15455  ptolemy  15498  coskpi  15522  logbrec  15634  mpodvdsmulf1o  15664  fsumdvdsmul  15665  lgslem1  15679  lgsval  15683  lgsval4  15699  lgsfcl3  15700  lgsdilem  15706  lgsdir2lem4  15710  lgsdir2lem5  15711  gausslemma2dlem5  15745  lgsquadlem2  15757  iedgedgg  15861  isuhgrm  15871  isushgrm  15872  isupgren  15895  isumgren  15905  isuspgren  15955  isusgren  15956  usgrstrrepeen  16029  wksfval  16035  ifpsnprss  16054  nninfsellemqall  16381