Theorem eqtr3id 2252

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 2209	. 2 |- A = B
3		eqtr3id.2	. 2 |- ( ph -> B = C )
4	2, 3	eqtrid 2250	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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  3eqtr3g  2261  csbeq1a  3102  ssdifeq0  3543  pofun  4359  opabbi2dv  4827  funimaexg  5358  fresin  5454  f1imacnv  5539  foimacnv  5540  fsn2  5754  fmptpr  5776  funiunfvdm  5832  funiunfvdmf  5833  fcof1o  5858  f1opw2  6152  fnexALT  6196  eqerlem  6651  pmresg  6763  mapsn  6777  en2  6912  fopwdom  6933  mapen  6943  fiintim  7028  xpfi  7029  sbthlemi8  7066  sbthlemi9  7067  ctssdccl  7213  exmidfodomrlemim  7309  mul02  8459  recdivap  8791  fzpreddisj  10193  fzshftral  10230  suprzubdc  10379  qbtwnrelemcalc  10398  frec2uzrdg  10554  frecuzrdgrcl  10555  frecuzrdgsuc  10559  frecuzrdgrclt  10560  frecuzrdgg  10561  seqf1oglem2  10665  binom3  10802  bcn2  10909  hashfz1  10928  hashunlem  10949  hashfacen  10981  cnrecnv  11221  resqrexlemnm  11329  amgm2  11429  2zsupmax  11537  xrmaxltsup  11569  xrmaxadd  11572  xrbdtri  11587  fisumss  11703  fsumcnv  11748  telfsumo  11777  fsumiun  11788  arisum2  11810  fprodssdc  11901  fprodsplitdc  11907  fprodsplit  11908  fprodcnv  11936  ege2le3  11982  efgt1p  12007  cos01bnd  12069  dfgcd3  12331  eucalgval  12376  sqrt2irrlem  12483  pcid  12647  4sqlem15  12728  4sqlem16  12729  setsslid  12883  ressinbasd  12906  xpsff1o  13181  grpressid  13393  crng2idl  14293  znleval  14415  baspartn  14522  txdis1cn  14750  cnmpt21  14763  cnmpt22  14766  hmeores  14787  metreslem  14852  remetdval  15019  dvfvalap  15153  binom4  15451  mpodvdsmulf1o  15462  perfectlem2  15472  1lgs  15520  lgs1  15521  lgseisenlem1  15547  lgseisenlem2  15548  lgseisenlem3  15549  lgsquadlem2  15555  lgsquad2lem2  15559  nninfsellemqall  15952  nninfnfiinf  15960