Theorem syl5eq 2397

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
syl5eq.1	|- A = B
syl5eq.2	|- (ph -> B = C)

Assertion

Ref	Expression
syl5eq	|- (ph -> A = C)

Proof of Theorem syl5eq

Step	Hyp	Ref	Expression
1		syl5eq.1	. . 3 |- A = B
2	1	a1i 10	. 2 |- (ph -> A = B)
3		syl5eq.2	. 2 |- (ph -> B = C)
4	2, 3	eqtrd 2385	1 |- (ph -> A = C)

Syntax hints:   -> wi 4   = wceq 1642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2346

This theorem is referenced by:  syl5req  2398  syl5eqr  2399  3eqtr3a  2409  3eqtr4g  2410  csbtt  3148  csbvarg  3163  csbie2g  3182  rabbi2dva  3463  disjssun  3608  difprsn2  3848  difsnid  3854  intsng  3961  riinn0  4040  iinxsng  4042  rintn0  4056  prprc2  4122  prprc1  4123  pw1eqadj  4332  iotaval  4350  iotanul  4354  nnsucelrlem4  4427  ssfin  4470  dmxp  4923  resabs1  4992  resabs2  4993  resopab2  5001  resiima  5012  imasn  5018  ndmima  5025  xpdisj1  5047  xpdisj2  5048  resdisj  5050  rnxp  5051  dfco2a  5081  cores2  5091  fnun  5189  fnresdisj  5193  fnima  5201  f1orescnv  5301  resdif  5306  f1ococnv2  5309  fvprc  5325  tz6.12-1  5344  tz6.12-2  5346  fnrnfv  5364  fvun  5378  fvun2  5380  ressnop0  5436  fvunsn  5444  fvsnun2  5448  fvpr1  5449  funiunfv  5467  f1oiso2  5500  resoprab2  5582  fnoprabg  5585  ovidig  5593  ov6g  5600  ovconst2  5611  ndmovg  5613  ndmovcl  5614  ndmov  5615  caovmo  5645  elovex12  5648  fvmptnf  5723  fntxp  5804  fnpprod  5843  map0b  6024  enpw1  6062  sbthlem1  6203  dflec2  6210  nchoicelem7  6295