Theorem eqtr3id 2204

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

Syntax hints:   -> wi 4   = wceq 1335

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 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ext 2139

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

This theorem is referenced by:  3eqtr3g  2213  csbeq1a  3040  ssdifeq0  3477  pofun  4275  opabbi2dv  4738  funimaexg  5257  fresin  5351  f1imacnv  5434  foimacnv  5435  fsn2  5644  fmptpr  5662  funiunfvdm  5716  funiunfvdmf  5717  fcof1o  5742  f1opw2  6029  fnexALT  6064  eqerlem  6514  pmresg  6624  mapsn  6638  fopwdom  6784  mapen  6794  fiintim  6876  xpfi  6877  sbthlemi8  6911  sbthlemi9  6912  ctssdccl  7058  exmidfodomrlemim  7139  mul02  8267  recdivap  8596  fzpreddisj  9980  fzshftral  10017  qbtwnrelemcalc  10165  frec2uzrdg  10318  frecuzrdgrcl  10319  frecuzrdgsuc  10323  frecuzrdgrclt  10324  frecuzrdgg  10325  binom3  10545  bcn2  10650  hashfz1  10669  hashunlem  10690  hashfacen  10719  cnrecnv  10822  resqrexlemnm  10930  amgm2  11030  2zsupmax  11137  xrmaxltsup  11167  xrmaxadd  11170  xrbdtri  11185  fisumss  11301  fsumcnv  11346  telfsumo  11375  fsumiun  11386  arisum2  11408  fprodssdc  11499  fprodsplitdc  11505  fprodsplit  11506  fprodcnv  11534  ege2le3  11580  efgt1p  11605  cos01bnd  11667  suprzubdc  11852  dfgcd3  11910  eucalgval  11947  sqrt2irrlem  12052  pcid  12213  setsslid  12336  baspartn  12544  txdis1cn  12774  cnmpt21  12787  cnmpt22  12790  hmeores  12811  metreslem  12876  remetdval  13035  dvfvalap  13146  binom4  13393  nninfsellemqall  13684