ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl6eq Structured version   GIF version

Theorem syl6eq 2070
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6eq.1 (φA = B)
syl6eq.2 B = 𝐶
Assertion
Ref Expression
syl6eq (φA = 𝐶)

Proof of Theorem syl6eq
StepHypRef Expression
1 syl6eq.1 . 2 (φA = B)
2 syl6eq.2 . . 3 B = 𝐶
32a1i 9 . 2 (φB = 𝐶)
41, 3eqtrd 2054 1 (φA = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1228
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 1316  ax-gen 1318  ax-4 1381  ax-17 1400  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-cleq 2015
This theorem is referenced by:  syl6req  2071  syl6eqr  2072  3eqtr3g  2077  3eqtr4a  2080  cbvralcsf  2885  cbvrexcsf  2886  cbvreucsf  2887  cbvrabcsf  2888  csbprc  3239  un00  3240  disjssun  3262  disjpr2  3408  tppreq3  3447  diftpsn3  3479  preq12b  3515  intsng  3623  uniintsnr  3625  rint0  3628  riin0  3702  iununir  3712  intexr  3878  sucprc  4098  op1stbg  4160  elreldm  4487  xpeq0r  4673  xpdisj1  4674  xpdisj2  4675  resdisj  4678  xpima1  4694  xpima2m  4695  elxp4  4735  unixp0im  4781  uniabio  4804  iotass  4811  cnvresid  4899  funimacnv  4901  f1o00  5086  dffv4g  5100  fnrnfv  5145  feqresmpt  5152  dffn5imf  5153  funfvdm2f  5163  fvun1  5164  fvmpt2  5179  fndmin  5199  fmptcof  5256  fmptcos  5257  fvunsng  5282  fvpr1  5290  fnrnov  5569  offval  5642  ofrfval  5643  op1std  5698  op2ndd  5699  fmpt2co  5760  tpostpos  5801  rdgi0g  5886  rdgival  5889  frec0g  5902  2oconcl  5937  oasuc  5959  omv2  5960  nnm0r  5973  uniqs2  6077  nq0m0r  6311  genipv  6363  genpelvl  6366  genpelvu  6367  addresr  6548  mulresr  6549  axcnre  6575  bj-intexr  7278
  Copyright terms: Public domain W3C validator