Theorem eqtr3id 2254

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqtr3id.1	|- B = A
eqtr3id.2	|- ( ph -> B = C )

Assertion

Ref	Expression
eqtr3id	|- ( ph -> A = C )

Proof of Theorem eqtr3id

Step	Hyp	Ref	Expression
1		eqtr3id.1	. . 3 |- B = A
2	1	eqcomi 2211	. 2 |- A = B
3		eqtr3id.2	. 2 |- ( ph -> B = C )
4	2, 3	eqtrid 2252	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  3eqtr3g  2263  csbeq1a  3110  ssdifeq0  3551  pofun  4377  opabbi2dv  4845  funimaexg  5377  fresin  5476  f1imacnv  5561  foimacnv  5562  fsn2  5777  fmptpr  5799  funiunfvdm  5855  funiunfvdmf  5856  fcof1o  5881  f1opw2  6175  fnexALT  6219  eqerlem  6674  pmresg  6786  mapsn  6800  en2  6936  fopwdom  6958  mapen  6968  fiintim  7054  xpfi  7055  sbthlemi8  7092  sbthlemi9  7093  ctssdccl  7239  exmidfodomrlemim  7340  mul02  8494  recdivap  8826  fzpreddisj  10228  fzshftral  10265  suprzubdc  10416  qbtwnrelemcalc  10435  frec2uzrdg  10591  frecuzrdgrcl  10592  frecuzrdgsuc  10596  frecuzrdgrclt  10597  frecuzrdgg  10598  seqf1oglem2  10702  binom3  10839  bcn2  10946  hashfz1  10965  hashunlem  10986  hashfacen  11018  cnrecnv  11336  resqrexlemnm  11444  amgm2  11544  2zsupmax  11652  xrmaxltsup  11684  xrmaxadd  11687  xrbdtri  11702  fisumss  11818  fsumcnv  11863  telfsumo  11892  fsumiun  11903  arisum2  11925  fprodssdc  12016  fprodsplitdc  12022  fprodsplit  12023  fprodcnv  12051  ege2le3  12097  efgt1p  12122  cos01bnd  12184  dfgcd3  12446  eucalgval  12491  sqrt2irrlem  12598  pcid  12762  4sqlem15  12843  4sqlem16  12844  setsslid  12998  ressinbasd  13021  xpsff1o  13296  grpressid  13508  crng2idl  14408  znleval  14530  baspartn  14637  txdis1cn  14865  cnmpt21  14878  cnmpt22  14881  hmeores  14902  metreslem  14967  remetdval  15134  dvfvalap  15268  binom4  15566  mpodvdsmulf1o  15577  perfectlem2  15587  1lgs  15635  lgs1  15636  lgseisenlem1  15662  lgseisenlem2  15663  lgseisenlem3  15664  lgsquadlem2  15670  lgsquad2lem2  15674  nninfsellemqall  16154  nninfnfiinf  16162