Theorem eqtr3id 2281

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 2238	. 2 |- A = B
3		eqtr3id.2	. 2 |- ( ph -> B = C )
4	2, 3	eqtrid 2279	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 2216

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

This theorem is referenced by:  3eqtr3g  2290  csbeq1a  3150  ssdifeq0  3597  pofun  4439  opabbi2dv  4910  funimaexg  5446  fresin  5549  f1imacnv  5637  foimacnv  5638  fsn2  5857  fmptpr  5882  funiunfvdm  5943  funiunfvdmf  5944  fcof1o  5969  f1opw2  6270  fnexALT  6314  eqerlem  6812  pmresg  6924  mapsn  6939  en2  7079  fopwdom  7103  mapen  7113  fiintim  7205  xpfi  7206  sbthlemi8  7248  sbthlemi9  7249  ctssdccl  7416  exmidfodomrlemim  7518  mul02  8679  recdivap  9013  fzpreddisj  10431  fzshftral  10468  suprzubdc  10624  qbtwnrelemcalc  10643  frec2uzrdg  10799  frecuzrdgrcl  10800  frecuzrdgsuc  10804  frecuzrdgrclt  10805  frecuzrdgg  10806  seqf1oglem2  10910  binom3  11047  bcn2  11155  hashfz1  11175  hashunlem  11197  hashfacen  11237  hashtpg  11248  cnrecnv  11625  resqrexlemnm  11733  amgm2  11833  2zsupmax  11941  xrmaxltsup  11973  xrmaxadd  11976  xrbdtri  11991  fisumss  12108  fsumcnv  12153  telfsumo  12182  fsumiun  12193  arisum2  12215  fprodssdc  12306  fprodsplitdc  12312  fprodsplit  12313  fprodcnv  12341  ege2le3  12387  efgt1p  12412  cos01bnd  12474  dfgcd3  12736  eucalgval  12781  sqrt2irrlem  12888  pcid  13052  4sqlem15  13133  4sqlem16  13134  ballotfilemic  13199  setsslid  13352  ressinbasd  13376  xpsff1o  13618  grpressid  13821  crng2idl  14810  znleval  14932  baspartn  15046  txdis1cn  15274  cnmpt21  15287  cnmpt22  15290  hmeores  15311  metreslem  15376  remetdval  15543  dvfvalap  15677  binom4  15975  mpodvdsmulf1o  15989  perfectlem2  15999  1lgs  16047  lgs1  16048  lgseisenlem1  16074  lgseisenlem2  16075  lgseisenlem3  16076  lgsquadlem2  16082  lgsquad2lem2  16086  vtxdfifiun  16423  vtxdumgrfival  16424  nninfsellemqall  16934  nninfnfiinf  16942  repiecege0  16952