Theorem eqtr3id 2234

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

Syntax hints:   -> wi 4   = wceq 1363

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 1457  ax-gen 1459  ax-4 1520  ax-17 1536  ax-ext 2169

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

This theorem is referenced by:  3eqtr3g  2243  csbeq1a  3078  ssdifeq0  3517  pofun  4324  opabbi2dv  4788  funimaexg  5312  fresin  5406  f1imacnv  5490  foimacnv  5491  fsn2  5703  fmptpr  5721  funiunfvdm  5777  funiunfvdmf  5778  fcof1o  5803  f1opw2  6091  fnexALT  6126  eqerlem  6580  pmresg  6690  mapsn  6704  fopwdom  6850  mapen  6860  fiintim  6942  xpfi  6943  sbthlemi8  6977  sbthlemi9  6978  ctssdccl  7124  exmidfodomrlemim  7214  mul02  8358  recdivap  8689  fzpreddisj  10085  fzshftral  10122  qbtwnrelemcalc  10270  frec2uzrdg  10423  frecuzrdgrcl  10424  frecuzrdgsuc  10428  frecuzrdgrclt  10429  frecuzrdgg  10430  binom3  10652  bcn2  10758  hashfz1  10777  hashunlem  10798  hashfacen  10830  cnrecnv  10933  resqrexlemnm  11041  amgm2  11141  2zsupmax  11248  xrmaxltsup  11280  xrmaxadd  11283  xrbdtri  11298  fisumss  11414  fsumcnv  11459  telfsumo  11488  fsumiun  11499  arisum2  11521  fprodssdc  11612  fprodsplitdc  11618  fprodsplit  11619  fprodcnv  11647  ege2le3  11693  efgt1p  11718  cos01bnd  11780  suprzubdc  11967  dfgcd3  12025  eucalgval  12068  sqrt2irrlem  12175  pcid  12337  setsslid  12527  ressinbasd  12548  xpsff1o  12787  grpressid  12958  crng2idl  13718  baspartn  13846  txdis1cn  14074  cnmpt21  14087  cnmpt22  14090  hmeores  14111  metreslem  14176  remetdval  14335  dvfvalap  14446  binom4  14693  1lgs  14740  lgs1  14741  lgseisenlem1  14746  lgseisenlem2  14747  nninfsellemqall  15061