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  4457  opabbi2dv  4929  funimaexg  5465  fresin  5568  f1imacnv  5656  foimacnv  5657  fsn2  5882  fmptpr  5907  funiunfvdm  5969  funiunfvdmf  5970  fcof1o  5995  f1opw2  6296  fnexALT  6340  eqerlem  6838  pmresg  6957  mapsn  6972  en2  7112  fopwdom  7136  mapen  7146  fiintim  7238  xpfi  7239  sbthlemi8  7281  sbthlemi9  7282  ctssdccl  7451  exmidfodomrlemim  7553  mul02  8714  recdivap  9048  fzpreddisj  10478  fzshftral  10515  suprzubdc  10671  qbtwnrelemcalc  10690  frec2uzrdg  10846  frecuzrdgrcl  10847  frecuzrdgsuc  10851  frecuzrdgrclt  10852  frecuzrdgg  10853  seqf1oglem2  10957  binom3  11094  bcn2  11202  hashfz1  11222  hashunlem  11244  hashfacen  11284  hashtpg  11299  cnrecnv  11676  resqrexlemnm  11784  amgm2  11884  2zsupmax  11992  xrmaxltsup  12024  xrmaxadd  12027  xrbdtri  12042  fisumss  12159  fsumcnv  12204  telfsumo  12233  fsumiun  12244  arisum2  12266  fprodssdc  12357  fprodsplitdc  12363  fprodsplit  12364  fprodcnv  12392  ege2le3  12438  efgt1p  12463  cos01bnd  12525  dfgcd3  12787  eucalgval  12832  sqrt2irrlem  12939  pcid  13103  4sqlem15  13184  4sqlem16  13185  ballotfilemic  13250  setsslid  13403  ressinbasd  13428  xpsff1o  13670  grpressid  13866  gsumf1ofi  14160  gsumconstcmn  14166  crng2idl  14868  znleval  14988  baspartn  15151  txdis1cn  15379  cnmpt21  15392  cnmpt22  15395  hmeores  15416  metreslem  15481  remetdval  15648  dvfvalap  15782  binom4  16081  mpodvdsmulf1o  16104  perfectlem2  16114  1lgs  16162  lgs1  16163  lgseisenlem1  16189  lgseisenlem2  16190  lgseisenlem3  16191  lgsquadlem2  16197  lgsquad2lem2  16201  vtxdfifiun  16538  vtxdumgrfival  16539  nninfsellemqall  17058  nninfnfiinf  17066  repiecege0  17076