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 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  3eqtr3g  2287  csbeq1a  3137  ssdifeq0  3579  pofun  4415  opabbi2dv  4885  funimaexg  5421  fresin  5523  f1imacnv  5609  foimacnv  5610  fsn2  5829  fmptpr  5854  funiunfvdm  5914  funiunfvdmf  5915  fcof1o  5940  f1opw2  6239  fnexALT  6282  eqerlem  6776  pmresg  6888  mapsn  6902  en2  7041  fopwdom  7065  mapen  7075  fiintim  7166  xpfi  7167  sbthlemi8  7206  sbthlemi9  7207  ctssdccl  7370  exmidfodomrlemim  7472  mul02  8625  recdivap  8957  fzpreddisj  10368  fzshftral  10405  suprzubdc  10559  qbtwnrelemcalc  10578  frec2uzrdg  10734  frecuzrdgrcl  10735  frecuzrdgsuc  10739  frecuzrdgrclt  10740  frecuzrdgg  10741  seqf1oglem2  10845  binom3  10982  bcn2  11089  hashfz1  11108  hashunlem  11130  hashfacen  11163  hashtpg  11174  cnrecnv  11550  resqrexlemnm  11658  amgm2  11758  2zsupmax  11866  xrmaxltsup  11898  xrmaxadd  11901  xrbdtri  11916  fisumss  12033  fsumcnv  12078  telfsumo  12107  fsumiun  12118  arisum2  12140  fprodssdc  12231  fprodsplitdc  12237  fprodsplit  12238  fprodcnv  12266  ege2le3  12312  efgt1p  12337  cos01bnd  12399  dfgcd3  12661  eucalgval  12706  sqrt2irrlem  12813  pcid  12977  4sqlem15  13058  4sqlem16  13059  setsslid  13213  ressinbasd  13237  xpsff1o  13512  grpressid  13724  crng2idl  14627  znleval  14749  baspartn  14861  txdis1cn  15089  cnmpt21  15102  cnmpt22  15105  hmeores  15126  metreslem  15191  remetdval  15358  dvfvalap  15492  binom4  15790  mpodvdsmulf1o  15804  perfectlem2  15814  1lgs  15862  lgs1  15863  lgseisenlem1  15889  lgseisenlem2  15890  lgseisenlem3  15891  lgsquadlem2  15897  lgsquad2lem2  15901  vtxdfifiun  16238  vtxdumgrfival  16239  nninfsellemqall  16741  nninfnfiinf  16749  repiecege0  16759