Theorem eqtr3id 2276

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

Syntax hints:   -> wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  3eqtr3g  2285  csbeq1a  3133  ssdifeq0  3574  pofun  4403  opabbi2dv  4871  funimaexg  5405  fresin  5504  f1imacnv  5589  foimacnv  5590  fsn2  5809  fmptpr  5831  funiunfvdm  5887  funiunfvdmf  5888  fcof1o  5913  f1opw2  6212  fnexALT  6256  eqerlem  6711  pmresg  6823  mapsn  6837  en2  6973  fopwdom  6997  mapen  7007  fiintim  7093  xpfi  7094  sbthlemi8  7131  sbthlemi9  7132  ctssdccl  7278  exmidfodomrlemim  7379  mul02  8533  recdivap  8865  fzpreddisj  10267  fzshftral  10304  suprzubdc  10456  qbtwnrelemcalc  10475  frec2uzrdg  10631  frecuzrdgrcl  10632  frecuzrdgsuc  10636  frecuzrdgrclt  10637  frecuzrdgg  10638  seqf1oglem2  10742  binom3  10879  bcn2  10986  hashfz1  11005  hashunlem  11026  hashfacen  11058  cnrecnv  11421  resqrexlemnm  11529  amgm2  11629  2zsupmax  11737  xrmaxltsup  11769  xrmaxadd  11772  xrbdtri  11787  fisumss  11903  fsumcnv  11948  telfsumo  11977  fsumiun  11988  arisum2  12010  fprodssdc  12101  fprodsplitdc  12107  fprodsplit  12108  fprodcnv  12136  ege2le3  12182  efgt1p  12207  cos01bnd  12269  dfgcd3  12531  eucalgval  12576  sqrt2irrlem  12683  pcid  12847  4sqlem15  12928  4sqlem16  12929  setsslid  13083  ressinbasd  13107  xpsff1o  13382  grpressid  13594  crng2idl  14495  znleval  14617  baspartn  14724  txdis1cn  14952  cnmpt21  14965  cnmpt22  14968  hmeores  14989  metreslem  15054  remetdval  15221  dvfvalap  15355  binom4  15653  mpodvdsmulf1o  15664  perfectlem2  15674  1lgs  15722  lgs1  15723  lgseisenlem1  15749  lgseisenlem2  15750  lgseisenlem3  15751  lgsquadlem2  15757  lgsquad2lem2  15761  nninfsellemqall  16381  nninfnfiinf  16389