Theorem eqtr3id 2285

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  3eqtr3g  2294  csbeq1a  3156  ssdifeq0  3610  pofun  4459  opabbi2dv  4931  funimaexg  5468  fresin  5571  f1imacnv  5659  foimacnv  5660  fsn2  5885  fmptpr  5910  funiunfvdm  5972  funiunfvdmf  5973  fcof1o  5998  f1opw2  6299  fnexALT  6344  eqerlem  6843  pmresg  6962  mapsn  6978  en2  7118  fopwdom  7142  mapen  7152  fiintim  7244  xpfi  7245  sbthlemi8  7288  sbthlemi9  7289  ctssdccl  7457  exmidfodomrlemim  7559  mul02  8721  recdivap  9056  fzpreddisj  10494  fzshftral  10531  suprzubdc  10687  qbtwnrelemcalc  10706  frec2uzrdg  10866  frecuzrdgrcl  10867  frecuzrdgsuc  10871  frecuzrdgrclt  10872  frecuzrdgg  10873  seqf1oglem2  10977  binom3  11114  bcn2  11223  hashfz1  11243  hashunlem  11265  hashfacen  11305  hashtpg  11320  cnrecnv  11697  resqrexlemnm  11805  amgm2  11906  2zsupmax  12014  xrmaxltsup  12048  xrmaxadd  12051  xrbdtri  12066  fisumss  12183  fsumcnv  12228  telfsumo  12257  fsumiun  12268  arisum2  12290  fprodssdc  12381  fprodsplitdc  12387  fprodsplit  12388  fprodcnv  12416  ege2le3  12462  efgt1p  12487  cos01bnd  12549  dfgcd3  12811  eucalgval  12856  sqrt2irrlem  12964  pcid  13131  4sqlem15  13212  4sqlem16  13213  ballotfilemic  13307  setsslid  13460  ressinbasd  13486  xpsff1o  13728  grpressid  13924  gsumf1ofi  14249  gsumconstcmn  14265  crng2idl  14976  znleval  15096  psrass1filem  15186  baspartn  15293  txdis1cn  15521  cnmpt21  15534  cnmpt22  15537  hmeores  15558  metreslem  15623  remetdval  15790  dvfvalap  15924  binom4  16236  mpodvdsmulf1o  16301  ppiqub  16310  chtublem  16312  perfectlem2  16317  bposlem6  16333  bposlem9  16336  1lgs  16384  lgs1  16385  lgseisenlem1  16411  lgseisenlem2  16412  lgseisenlem3  16413  lgsquadlem2  16419  lgsquad2lem2  16423  vtxdfifiun  16760  vtxdumgrfival  16761  nninfsellemqall  17281  nninfnfiinf  17289  repiecege0  17299