Theorem syl5eq 2397

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

Hypotheses

Ref	Expression
syl5eq.1	⊢ A = B
syl5eq.2	⊢ (φ → B = C)

Assertion

Ref	Expression
syl5eq	⊢ (φ → A = C)

Proof of Theorem syl5eq

Step	Hyp	Ref	Expression
1		syl5eq.1	. . 3 ⊢ A = B
2	1	a1i 10	. 2 ⊢ (φ → A = B)
3		syl5eq.2	. 2 ⊢ (φ → B = C)
4	2, 3	eqtrd 2385	1 ⊢ (φ → 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  3149  csbvarg  3164  csbie2g  3183  rabbi2dva  3464  disjssun  3609  difprsn2  3849  difsnid  3855  intsng  3962  riinn0  4041  iinxsng  4043  rintn0  4057  prprc2  4123  prprc1  4124  pw1eqadj  4333  iotaval  4351  iotanul  4355  nnsucelrlem4  4428  ssfin  4471  dmxp  4924  resabs1  4993  resabs2  4994  resopab2  5002  resiima  5013  imasn  5019  ndmima  5026  xpdisj1  5048  xpdisj2  5049  resdisj  5051  rnxp  5052  dfco2a  5082  cores2  5092  fnun  5190  fnresdisj  5194  fnima  5202  f1orescnv  5302  resdif  5307  f1ococnv2  5310  fvprc  5326  tz6.12-1  5345  tz6.12-2  5347  fnrnfv  5365  fvun  5379  fvun2  5381  ressnop0  5437  fvunsn  5445  fvsnun2  5449  fvpr1  5450  funiunfv  5468  f1oiso2  5501  resoprab2  5583  fnoprabg  5586  ovidig  5594  ov6g  5601  ovconst2  5612  ndmovg  5614  ndmovcl  5615  ndmov  5616  caovmo  5646  elovex12  5649  fvmptnf  5724  fntxp  5805  fnpprod  5844  map0b  6025  enpw1  6063  sbthlem1  6204  dflec2  6211  nchoicelem7  6296