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  7452  exmidfodomrlemim  7554  mul02  8716  recdivap  9051  fzpreddisj  10489  fzshftral  10526  suprzubdc  10682  qbtwnrelemcalc  10701  frec2uzrdg  10861  frecuzrdgrcl  10862  frecuzrdgsuc  10866  frecuzrdgrclt  10867  frecuzrdgg  10868  seqf1oglem2  10972  binom3  11109  bcn2  11218  hashfz1  11238  hashunlem  11260  hashfacen  11300  hashtpg  11315  cnrecnv  11692  resqrexlemnm  11800  amgm2  11901  2zsupmax  12009  xrmaxltsup  12043  xrmaxadd  12046  xrbdtri  12061  fisumss  12178  fsumcnv  12223  telfsumo  12252  fsumiun  12263  arisum2  12285  fprodssdc  12376  fprodsplitdc  12382  fprodsplit  12383  fprodcnv  12411  ege2le3  12457  efgt1p  12482  cos01bnd  12544  dfgcd3  12806  eucalgval  12851  sqrt2irrlem  12959  pcid  13126  4sqlem15  13207  4sqlem16  13208  ballotfilemic  13302  setsslid  13455  ressinbasd  13481  xpsff1o  13723  grpressid  13919  gsumf1ofi  14244  gsumconstcmn  14250  crng2idl  14952  znleval  15072  baspartn  15242  txdis1cn  15470  cnmpt21  15483  cnmpt22  15486  hmeores  15507  metreslem  15572  remetdval  15739  dvfvalap  15873  binom4  16180  mpodvdsmulf1o  16245  ppiqub  16254  chtublem  16256  perfectlem2  16261  bposlem6  16277  bposlem9  16280  1lgs  16328  lgs1  16329  lgseisenlem1  16355  lgseisenlem2  16356  lgseisenlem3  16357  lgsquadlem2  16363  lgsquad2lem2  16367  vtxdfifiun  16704  vtxdumgrfival  16705  nninfsellemqall  17224  nninfnfiinf  17232  repiecege0  17242