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  5506  f1imacnv  5591  foimacnv  5592  fsn2  5811  fmptpr  5835  funiunfvdm  5893  funiunfvdmf  5894  fcof1o  5919  f1opw2  6218  fnexALT  6262  eqerlem  6719  pmresg  6831  mapsn  6845  en2  6981  fopwdom  7005  mapen  7015  fiintim  7104  xpfi  7105  sbthlemi8  7142  sbthlemi9  7143  ctssdccl  7289  exmidfodomrlemim  7390  mul02  8544  recdivap  8876  fzpreddisj  10279  fzshftral  10316  suprzubdc  10468  qbtwnrelemcalc  10487  frec2uzrdg  10643  frecuzrdgrcl  10644  frecuzrdgsuc  10648  frecuzrdgrclt  10649  frecuzrdgg  10650  seqf1oglem2  10754  binom3  10891  bcn2  10998  hashfz1  11017  hashunlem  11038  hashfacen  11071  cnrecnv  11437  resqrexlemnm  11545  amgm2  11645  2zsupmax  11753  xrmaxltsup  11785  xrmaxadd  11788  xrbdtri  11803  fisumss  11919  fsumcnv  11964  telfsumo  11993  fsumiun  12004  arisum2  12026  fprodssdc  12117  fprodsplitdc  12123  fprodsplit  12124  fprodcnv  12152  ege2le3  12198  efgt1p  12223  cos01bnd  12285  dfgcd3  12547  eucalgval  12592  sqrt2irrlem  12699  pcid  12863  4sqlem15  12944  4sqlem16  12945  setsslid  13099  ressinbasd  13123  xpsff1o  13398  grpressid  13610  crng2idl  14511  znleval  14633  baspartn  14740  txdis1cn  14968  cnmpt21  14981  cnmpt22  14984  hmeores  15005  metreslem  15070  remetdval  15237  dvfvalap  15371  binom4  15669  mpodvdsmulf1o  15680  perfectlem2  15690  1lgs  15738  lgs1  15739  lgseisenlem1  15765  lgseisenlem2  15766  lgseisenlem3  15767  lgsquadlem2  15773  lgsquad2lem2  15777  vtxdfifiun  16057  vtxdumgrfival  16058  nninfsellemqall  16469  nninfnfiinf  16477