Theorem syl5eq 2081

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 2069	1 |- (ph -> A = C)

Syntax hints:   -> wi 4   = wceq 1242

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 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019

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

This theorem is referenced by:  syl5req  2082  syl5eqr  2083  3eqtr3a  2093  3eqtr4g  2094  csbtt  2856  csbvarg  2871  csbie2g  2890  rabbi2dva  3139  csbprc  3256  disjssun  3279  disjpr2  3425  prprc2  3470  difprsn2  3495  opprc  3561  intsng  3640  riinm  3720  iinxsng  3721  rintm  3735  sucprc  4115  unisucg  4117  xpriindim  4417  relop  4429  dmxpm  4498  riinint  4536  resabs1  4583  resabs2  4584  resima2  4587  xpssres  4588  resopab2  4598  imasng  4633  ndmima  4645  xpdisj1  4690  xpdisj2  4691  djudisj  4693  resdisj  4694  rnxpm  4695  xpima1  4710  xpima2m  4711  dmsnsnsng  4741  rnsnopg  4742  rnpropg  4743  mptiniseg  4758  dfco2a  4764  relcoi1  4792  unixpm  4796  iotaval  4821  funtp  4895  fnun  4948  fnresdisj  4952  fnima  4960  fnimaeq0  4963  fcoi1  5013  f1orescnv  5085  foun  5088  resdif  5091  tz6.12-2  5112  fveu  5113  tz6.12-1  5143  fvun2  5183  fvopab3ig  5189  f1oresrab  5272  dfmptg  5285  ressnop0  5287  fvunsng  5300  fsnunfv  5306  fvpr1  5308  fvpr2  5309  fvpr1g  5310  fvpr2g  5311  fvtp1g  5312  fvtp2g  5313  fvtp3g  5314  fvtp2  5316  fvtp3  5317  f1oiso2  5409  riotaund  5445  ovprc  5482  resoprab2  5540  fnoprabg  5544  ovidig  5560  ovigg  5563  ov6g  5580  ovconst2  5594  offval2  5668  ot1stg  5721  ot2ndg  5722  ot3rdgg  5723  fmpt2co  5779  tpostpos2  5821  rdgisuc1  5911  frec0g  5922  frecsuclem1  5926  frecsuclem2  5928  frecrdg  5931  oasuc  5983  oa1suc  5986  omsuc  5990  nnm1  6033  nnm2  6034  dfec2  6045  errn  6064  1qec  6372  mulidnq  6373  addpinq1  6447  0idsr  6695  1idsr  6696  mulresr  6735  pitonnlem2  6743  ax1rid  6761  axcnre  6765  negid  7054  subneg  7056  negneg  7057  2times  7816  rexneg  8513  fseq1p1m1  8726  fzosplitprm1  8860  frec2uz0d  8866  frec2uzrdg  8876  frecuzrdg0  8881  iseqval  8900  sqval  8966  binom3  9019  reim0  9089  remullem  9099