Theorem eqtr3id 2285

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  3eqtr3g  2294  csbeq1a  3156  ssdifeq0  3610  pofun  4457  opabbi2dv  4929  funimaexg  5465  fresin  5568  f1imacnv  5656  foimacnv  5657  fsn2  5882  fmptpr  5907  funiunfvdm  5969  funiunfvdmf  5970  fcof1o  5995  f1opw2  6296  fnexALT  6340  eqerlem  6838  pmresg  6957  mapsn  6972  en2  7112  fopwdom  7136  mapen  7146  fiintim  7238  xpfi  7239  sbthlemi8  7281  sbthlemi9  7282  ctssdccl  7451  exmidfodomrlemim  7553  mul02  8715  recdivap  9050  fzpreddisj  10488  fzshftral  10525  suprzubdc  10681  qbtwnrelemcalc  10700  frec2uzrdg  10859  frecuzrdgrcl  10860  frecuzrdgsuc  10864  frecuzrdgrclt  10865  frecuzrdgg  10866  seqf1oglem2  10970  binom3  11107  bcn2  11216  hashfz1  11236  hashunlem  11258  hashfacen  11298  hashtpg  11313  cnrecnv  11690  resqrexlemnm  11798  amgm2  11899  2zsupmax  12007  xrmaxltsup  12040  xrmaxadd  12043  xrbdtri  12058  fisumss  12175  fsumcnv  12220  telfsumo  12249  fsumiun  12260  arisum2  12282  fprodssdc  12373  fprodsplitdc  12379  fprodsplit  12380  fprodcnv  12408  ege2le3  12454  efgt1p  12479  cos01bnd  12541  dfgcd3  12803  eucalgval  12848  sqrt2irrlem  12956  pcid  13123  4sqlem15  13204  4sqlem16  13205  ballotfilemic  13299  setsslid  13452  ressinbasd  13477  xpsff1o  13719  grpressid  13915  gsumf1ofi  14209  gsumconstcmn  14215  crng2idl  14917  znleval  15037  baspartn  15200  txdis1cn  15428  cnmpt21  15441  cnmpt22  15444  hmeores  15465  metreslem  15530  remetdval  15697  dvfvalap  15831  binom4  16138  mpodvdsmulf1o  16185  ppiqub  16194  perfectlem2  16198  1lgs  16260  lgs1  16261  lgseisenlem1  16287  lgseisenlem2  16288  lgseisenlem3  16289  lgsquadlem2  16295  lgsquad2lem2  16299  vtxdfifiun  16636  vtxdumgrfival  16637  nninfsellemqall  17156  nninfnfiinf  17164  repiecege0  17174