Theorem eqtr3id 2243

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

Syntax hints:   -> wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  3eqtr3g  2252  csbeq1a  3093  ssdifeq0  3534  pofun  4348  opabbi2dv  4816  funimaexg  5343  fresin  5439  f1imacnv  5524  foimacnv  5525  fsn2  5739  fmptpr  5757  funiunfvdm  5813  funiunfvdmf  5814  fcof1o  5839  f1opw2  6133  fnexALT  6177  eqerlem  6632  pmresg  6744  mapsn  6758  fopwdom  6906  mapen  6916  fiintim  7001  xpfi  7002  sbthlemi8  7039  sbthlemi9  7040  ctssdccl  7186  exmidfodomrlemim  7280  mul02  8430  recdivap  8762  fzpreddisj  10163  fzshftral  10200  suprzubdc  10343  qbtwnrelemcalc  10362  frec2uzrdg  10518  frecuzrdgrcl  10519  frecuzrdgsuc  10523  frecuzrdgrclt  10524  frecuzrdgg  10525  seqf1oglem2  10629  binom3  10766  bcn2  10873  hashfz1  10892  hashunlem  10913  hashfacen  10945  cnrecnv  11092  resqrexlemnm  11200  amgm2  11300  2zsupmax  11408  xrmaxltsup  11440  xrmaxadd  11443  xrbdtri  11458  fisumss  11574  fsumcnv  11619  telfsumo  11648  fsumiun  11659  arisum2  11681  fprodssdc  11772  fprodsplitdc  11778  fprodsplit  11779  fprodcnv  11807  ege2le3  11853  efgt1p  11878  cos01bnd  11940  dfgcd3  12202  eucalgval  12247  sqrt2irrlem  12354  pcid  12518  4sqlem15  12599  4sqlem16  12600  setsslid  12754  ressinbasd  12777  xpsff1o  13051  grpressid  13263  crng2idl  14163  znleval  14285  baspartn  14370  txdis1cn  14598  cnmpt21  14611  cnmpt22  14614  hmeores  14635  metreslem  14700  remetdval  14867  dvfvalap  15001  binom4  15299  mpodvdsmulf1o  15310  perfectlem2  15320  1lgs  15368  lgs1  15369  lgseisenlem1  15395  lgseisenlem2  15396  lgseisenlem3  15397  lgsquadlem2  15403  lgsquad2lem2  15407  nninfsellemqall  15746