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

Theorem syl6eq 2085
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 2069 1 (φA = 𝐶)
Colors of variables: wff set class
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:  syl6req  2086  syl6eqr  2087  3eqtr3g  2092  3eqtr4a  2095  cbvralcsf  2902  cbvrexcsf  2903  cbvreucsf  2904  cbvrabcsf  2905  csbprc  3256  un00  3257  disjssun  3279  disjpr2  3425  tppreq3  3464  diftpsn3  3496  preq12b  3532  intsng  3640  uniintsnr  3642  rint0  3645  riin0  3719  iununir  3729  intexr  3895  sucprc  4115  op1stbg  4176  elreldm  4503  xpeq0r  4689  xpdisj1  4690  xpdisj2  4691  resdisj  4694  xpima1  4710  xpima2m  4711  elxp4  4751  unixp0im  4797  uniabio  4820  iotass  4827  cnvresid  4916  funimacnv  4918  f1o00  5104  dffv4g  5118  fnrnfv  5163  feqresmpt  5170  dffn5imf  5171  funfvdm2f  5181  fvun1  5182  fvmpt2  5197  fndmin  5217  fmptcof  5274  fmptcos  5275  fvunsng  5300  fvpr1  5308  fnrnov  5588  offval  5661  ofrfval  5662  op1std  5717  op2ndd  5718  fmpt2co  5779  tpostpos  5820  rdgival  5909  frec0g  5922  2oconcl  5961  om0  5977  oei0  5978  oasuc  5983  omv2  5984  nnm0r  5997  uniqs2  6102  en1  6215  en1bg  6216  fundmen  6222  xpsnen  6231  xpcomco  6236  xpdom2  6241  nq0m0r  6438  addpinq1  6446  genipv  6491  genpelvl  6494  genpelvu  6495  addresr  6694  mulresr  6695  axcnre  6725  add20  7224  rimul  7329  rereim  7330  mulreim  7348  nnm1nn0  7959  znegcl  8012  peano2z  8017  nneoor  8076  nn0ind-raph  8091  xnegneg  8476  xltnegi  8478  fzo0to2pr  8804  frecfzennn  8844  exp0  8873  expp1  8876  expnegap0  8877  1exp  8898  mulexp  8908  sq0i  8958  bernneq  8982  imre  9039  reim0b  9050  rereb  9051  bj-intexr  9293
  Copyright terms: Public domain W3C validator