Theorem eqtr3id 2278

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 2235	. 2 |- A = B
3		eqtr3id.2	. 2 |- ( ph -> B = C )
4	2, 3	eqtrid 2276	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  3eqtr3g  2287  csbeq1a  3136  ssdifeq0  3577  pofun  4409  opabbi2dv  4879  funimaexg  5414  fresin  5515  f1imacnv  5600  foimacnv  5601  fsn2  5821  fmptpr  5846  funiunfvdm  5904  funiunfvdmf  5905  fcof1o  5930  f1opw2  6229  fnexALT  6273  eqerlem  6733  pmresg  6845  mapsn  6859  en2  6998  fopwdom  7022  mapen  7032  fiintim  7123  xpfi  7124  sbthlemi8  7163  sbthlemi9  7164  ctssdccl  7310  exmidfodomrlemim  7412  mul02  8566  recdivap  8898  fzpreddisj  10306  fzshftral  10343  suprzubdc  10497  qbtwnrelemcalc  10516  frec2uzrdg  10672  frecuzrdgrcl  10673  frecuzrdgsuc  10677  frecuzrdgrclt  10678  frecuzrdgg  10679  seqf1oglem2  10783  binom3  10920  bcn2  11027  hashfz1  11046  hashunlem  11068  hashfacen  11101  hashtpg  11112  cnrecnv  11488  resqrexlemnm  11596  amgm2  11696  2zsupmax  11804  xrmaxltsup  11836  xrmaxadd  11839  xrbdtri  11854  fisumss  11971  fsumcnv  12016  telfsumo  12045  fsumiun  12056  arisum2  12078  fprodssdc  12169  fprodsplitdc  12175  fprodsplit  12176  fprodcnv  12204  ege2le3  12250  efgt1p  12275  cos01bnd  12337  dfgcd3  12599  eucalgval  12644  sqrt2irrlem  12751  pcid  12915  4sqlem15  12996  4sqlem16  12997  setsslid  13151  ressinbasd  13175  xpsff1o  13450  grpressid  13662  crng2idl  14564  znleval  14686  baspartn  14793  txdis1cn  15021  cnmpt21  15034  cnmpt22  15037  hmeores  15058  metreslem  15123  remetdval  15290  dvfvalap  15424  binom4  15722  mpodvdsmulf1o  15733  perfectlem2  15743  1lgs  15791  lgs1  15792  lgseisenlem1  15818  lgseisenlem2  15819  lgseisenlem3  15820  lgsquadlem2  15826  lgsquad2lem2  15830  vtxdfifiun  16167  vtxdumgrfival  16168  nninfsellemqall  16668  nninfnfiinf  16676