Theorem eqtr3id 2213

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

Syntax hints:   -> wi 4   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  3eqtr3g  2222  csbeq1a  3054  ssdifeq0  3491  pofun  4290  opabbi2dv  4753  funimaexg  5272  fresin  5366  f1imacnv  5449  foimacnv  5450  fsn2  5659  fmptpr  5677  funiunfvdm  5731  funiunfvdmf  5732  fcof1o  5757  f1opw2  6044  fnexALT  6079  eqerlem  6532  pmresg  6642  mapsn  6656  fopwdom  6802  mapen  6812  fiintim  6894  xpfi  6895  sbthlemi8  6929  sbthlemi9  6930  ctssdccl  7076  exmidfodomrlemim  7157  mul02  8285  recdivap  8614  fzpreddisj  10006  fzshftral  10043  qbtwnrelemcalc  10191  frec2uzrdg  10344  frecuzrdgrcl  10345  frecuzrdgsuc  10349  frecuzrdgrclt  10350  frecuzrdgg  10351  binom3  10572  bcn2  10677  hashfz1  10696  hashunlem  10717  hashfacen  10749  cnrecnv  10852  resqrexlemnm  10960  amgm2  11060  2zsupmax  11167  xrmaxltsup  11199  xrmaxadd  11202  xrbdtri  11217  fisumss  11333  fsumcnv  11378  telfsumo  11407  fsumiun  11418  arisum2  11440  fprodssdc  11531  fprodsplitdc  11537  fprodsplit  11538  fprodcnv  11566  ege2le3  11612  efgt1p  11637  cos01bnd  11699  suprzubdc  11885  dfgcd3  11943  eucalgval  11986  sqrt2irrlem  12093  pcid  12255  setsslid  12444  baspartn  12688  txdis1cn  12918  cnmpt21  12931  cnmpt22  12934  hmeores  12955  metreslem  13020  remetdval  13179  dvfvalap  13290  binom4  13537  1lgs  13584  lgs1  13585  nninfsellemqall  13895