Theorem eqtr3id 2252

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

Syntax hints:   -> wi 4   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  3eqtr3g  2261  csbeq1a  3102  ssdifeq0  3543  pofun  4360  opabbi2dv  4828  funimaexg  5359  fresin  5456  f1imacnv  5541  foimacnv  5542  fsn2  5756  fmptpr  5778  funiunfvdm  5834  funiunfvdmf  5835  fcof1o  5860  f1opw2  6154  fnexALT  6198  eqerlem  6653  pmresg  6765  mapsn  6779  en2  6914  fopwdom  6935  mapen  6945  fiintim  7030  xpfi  7031  sbthlemi8  7068  sbthlemi9  7069  ctssdccl  7215  exmidfodomrlemim  7311  mul02  8461  recdivap  8793  fzpreddisj  10195  fzshftral  10232  suprzubdc  10381  qbtwnrelemcalc  10400  frec2uzrdg  10556  frecuzrdgrcl  10557  frecuzrdgsuc  10561  frecuzrdgrclt  10562  frecuzrdgg  10563  seqf1oglem2  10667  binom3  10804  bcn2  10911  hashfz1  10930  hashunlem  10951  hashfacen  10983  cnrecnv  11254  resqrexlemnm  11362  amgm2  11462  2zsupmax  11570  xrmaxltsup  11602  xrmaxadd  11605  xrbdtri  11620  fisumss  11736  fsumcnv  11781  telfsumo  11810  fsumiun  11821  arisum2  11843  fprodssdc  11934  fprodsplitdc  11940  fprodsplit  11941  fprodcnv  11969  ege2le3  12015  efgt1p  12040  cos01bnd  12102  dfgcd3  12364  eucalgval  12409  sqrt2irrlem  12516  pcid  12680  4sqlem15  12761  4sqlem16  12762  setsslid  12916  ressinbasd  12939  xpsff1o  13214  grpressid  13426  crng2idl  14326  znleval  14448  baspartn  14555  txdis1cn  14783  cnmpt21  14796  cnmpt22  14799  hmeores  14820  metreslem  14885  remetdval  15052  dvfvalap  15186  binom4  15484  mpodvdsmulf1o  15495  perfectlem2  15505  1lgs  15553  lgs1  15554  lgseisenlem1  15580  lgseisenlem2  15581  lgseisenlem3  15582  lgsquadlem2  15588  lgsquad2lem2  15592  nninfsellemqall  15989  nninfnfiinf  15997