Theorem syl5eq 2084

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 9	. 2 |- ( ph -> A = B )
3		syl5eq.2	. 2 |- ( ph -> B = C )
4	2, 3	eqtrd 2072	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1243

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033

This theorem is referenced by:  syl5req  2085  syl5eqr  2086  3eqtr3a  2096  3eqtr4g  2097  csbtt  2862  csbvarg  2877  csbie2g  2896  rabbi2dva  3145  csbprc  3262  disjssun  3285  disjpr2  3434  prprc2  3479  difprsn2  3504  opprc  3570  intsng  3649  riinm  3729  iinxsng  3730  rintm  3744  sucprc  4149  unisucg  4151  xpriindim  4474  relop  4486  dmxpm  4555  riinint  4593  resabs1  4640  resabs2  4641  resima2  4644  xpssres  4645  resopab2  4655  imasng  4690  ndmima  4702  xpdisj1  4747  xpdisj2  4748  djudisj  4750  resdisj  4751  rnxpm  4752  xpima1  4767  xpima2m  4768  dmsnsnsng  4798  rnsnopg  4799  rnpropg  4800  mptiniseg  4815  dfco2a  4821  relcoi1  4849  unixpm  4853  iotaval  4878  funtp  4952  fnun  5005  fnresdisj  5009  fnima  5017  fnimaeq0  5020  fcoi1  5070  f1orescnv  5142  foun  5145  resdif  5148  tz6.12-2  5169  fveu  5170  tz6.12-1  5200  fvun2  5240  fvopab3ig  5246  f1oresrab  5329  dfmptg  5342  ressnop0  5344  fvunsng  5357  fsnunfv  5363  fvpr1  5365  fvpr2  5366  fvpr1g  5367  fvpr2g  5368  fvtp1g  5369  fvtp2g  5370  fvtp3g  5371  fvtp2  5373  fvtp3  5374  f1oiso2  5466  riotaund  5502  ovprc  5540  resoprab2  5598  fnoprabg  5602  ovidig  5618  ovigg  5621  ov6g  5638  ovconst2  5652  offval2  5726  ot1stg  5779  ot2ndg  5780  ot3rdgg  5781  fmpt2co  5837  algrflemg  5851  tpostpos2  5880  rdgisuc1  5971  frec0g  5983  frecsuclem1  5987  frecsuclem2  5989  frecrdg  5992  oasuc  6044  oa1suc  6047  omsuc  6051  nnm1  6097  nnm2  6098  dfec2  6109  errn  6128  phplem2  6316  1qec  6486  mulidnq  6487  addpinq1  6562  0idsr  6852  1idsr  6853  caucvgsrlemoffres  6884  caucvgsr  6886  mulresr  6914  pitonnlem2  6923  ax1rid  6951  axcnre  6955  negid  7258  subneg  7260  negneg  7261  2times  8038  rexneg  8743  fseq1p1m1  8956  fzosplitprm1  9090  intfracq  9162  frec2uz0d  9185  frec2uzrdg  9195  frecuzrdg0  9200  iseqval  9220  sqval  9312  binom3  9366  shftlem  9417  shftuz  9418  shftidt  9434  reim0  9461  remullem  9471  resqrexlemf1  9606  resqrexlemcalc3  9614  absexpzap  9676  absimle  9680  amgm2  9714  ialgr0  9883  ialgrp1  9885  ex-ceil  9896  qdencn  10124