Theorem eqtr3id 2279

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

Syntax hints:   -> wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  3eqtr3g  2288  csbeq1a  3147  ssdifeq0  3592  pofun  4433  opabbi2dv  4904  funimaexg  5440  fresin  5543  f1imacnv  5631  foimacnv  5632  fsn2  5851  fmptpr  5876  funiunfvdm  5936  funiunfvdmf  5937  fcof1o  5962  f1opw2  6261  fnexALT  6304  eqerlem  6798  pmresg  6910  mapsn  6925  en2  7065  fopwdom  7089  mapen  7099  fiintim  7191  xpfi  7192  sbthlemi8  7234  sbthlemi9  7235  ctssdccl  7402  exmidfodomrlemim  7504  mul02  8660  recdivap  8992  fzpreddisj  10405  fzshftral  10442  suprzubdc  10596  qbtwnrelemcalc  10615  frec2uzrdg  10771  frecuzrdgrcl  10772  frecuzrdgsuc  10776  frecuzrdgrclt  10777  frecuzrdgg  10778  seqf1oglem2  10882  binom3  11019  bcn2  11126  hashfz1  11146  hashunlem  11168  hashfacen  11208  hashtpg  11219  cnrecnv  11595  resqrexlemnm  11703  amgm2  11803  2zsupmax  11911  xrmaxltsup  11943  xrmaxadd  11946  xrbdtri  11961  fisumss  12078  fsumcnv  12123  telfsumo  12152  fsumiun  12163  arisum2  12185  fprodssdc  12276  fprodsplitdc  12282  fprodsplit  12283  fprodcnv  12311  ege2le3  12357  efgt1p  12382  cos01bnd  12444  dfgcd3  12706  eucalgval  12751  sqrt2irrlem  12858  pcid  13022  4sqlem15  13103  4sqlem16  13104  setsslid  13263  ressinbasd  13287  xpsff1o  13562  grpressid  13774  crng2idl  14679  znleval  14801  baspartn  14915  txdis1cn  15143  cnmpt21  15156  cnmpt22  15159  hmeores  15180  metreslem  15245  remetdval  15412  dvfvalap  15546  binom4  15844  mpodvdsmulf1o  15858  perfectlem2  15868  1lgs  15916  lgs1  15917  lgseisenlem1  15943  lgseisenlem2  15944  lgseisenlem3  15945  lgsquadlem2  15951  lgsquad2lem2  15955  vtxdfifiun  16292  vtxdumgrfival  16293  nninfsellemqall  16793  nninfnfiinf  16801  repiecege0  16811