Theorem eqtr3id 2211

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 2168	. 2 |- A = B
3		eqtr3id.2	. 2 |- ( ph -> B = C )
4	2, 3	syl5eq 2209	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1342

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-4 1497  ax-17 1513  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-cleq 2157

This theorem is referenced by:  3eqtr3g  2220  csbeq1a  3052  ssdifeq0  3489  pofun  4287  opabbi2dv  4750  funimaexg  5269  fresin  5363  f1imacnv  5446  foimacnv  5447  fsn2  5656  fmptpr  5674  funiunfvdm  5728  funiunfvdmf  5729  fcof1o  5754  f1opw2  6041  fnexALT  6076  eqerlem  6526  pmresg  6636  mapsn  6650  fopwdom  6796  mapen  6806  fiintim  6888  xpfi  6889  sbthlemi8  6923  sbthlemi9  6924  ctssdccl  7070  exmidfodomrlemim  7151  mul02  8279  recdivap  8608  fzpreddisj  10000  fzshftral  10037  qbtwnrelemcalc  10185  frec2uzrdg  10338  frecuzrdgrcl  10339  frecuzrdgsuc  10343  frecuzrdgrclt  10344  frecuzrdgg  10345  binom3  10566  bcn2  10671  hashfz1  10690  hashunlem  10711  hashfacen  10743  cnrecnv  10846  resqrexlemnm  10954  amgm2  11054  2zsupmax  11161  xrmaxltsup  11193  xrmaxadd  11196  xrbdtri  11211  fisumss  11327  fsumcnv  11372  telfsumo  11401  fsumiun  11412  arisum2  11434  fprodssdc  11525  fprodsplitdc  11531  fprodsplit  11532  fprodcnv  11560  ege2le3  11606  efgt1p  11631  cos01bnd  11693  suprzubdc  11879  dfgcd3  11937  eucalgval  11980  sqrt2irrlem  12087  pcid  12249  setsslid  12438  baspartn  12646  txdis1cn  12876  cnmpt21  12889  cnmpt22  12892  hmeores  12913  metreslem  12978  remetdval  13137  dvfvalap  13248  binom4  13495  nninfsellemqall  13788