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

Theorem syl6eq 2088
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6eq.1 (𝜑𝐴 = 𝐵)
syl6eq.2 𝐵 = 𝐶
Assertion
Ref Expression
syl6eq (𝜑𝐴 = 𝐶)

Proof of Theorem syl6eq
StepHypRef Expression
1 syl6eq.1 . 2 (𝜑𝐴 = 𝐵)
2 syl6eq.2 . . 3 𝐵 = 𝐶
32a1i 9 . 2 (𝜑𝐵 = 𝐶)
41, 3eqtrd 2072 1 (𝜑𝐴 = 𝐶)
Colors of variables: wff set class
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:  syl6req  2089  syl6eqr  2090  3eqtr3g  2095  3eqtr4a  2098  cbvralcsf  2908  cbvrexcsf  2909  cbvreucsf  2910  cbvrabcsf  2911  csbprc  3262  un00  3263  disjssun  3285  disjpr2  3434  tppreq3  3473  diftpsn3  3505  preq12b  3541  intsng  3649  uniintsnr  3651  rint0  3654  riin0  3728  iununir  3738  intexr  3904  sucprc  4149  op1stbg  4210  elreldm  4560  xpeq0r  4746  xpdisj1  4747  xpdisj2  4748  resdisj  4751  xpima1  4767  xpima2m  4768  elxp4  4808  unixp0im  4854  uniabio  4877  iotass  4884  cnvresid  4973  funimacnv  4975  f1o00  5161  dffv4g  5175  fnrnfv  5220  feqresmpt  5227  dffn5imf  5228  funfvdm2f  5238  fvun1  5239  fvmpt2  5254  fndmin  5274  fmptcof  5331  fmptcos  5332  fvunsng  5357  fvpr1  5365  fnrnov  5646  offval  5719  ofrfval  5720  op1std  5775  op2ndd  5776  fmpt2co  5837  tpostpos  5879  rdgival  5969  frec0g  5983  2oconcl  6022  om0  6038  oei0  6039  oasuc  6044  omv2  6045  nnm0r  6058  uniqs2  6166  en1  6279  en1bg  6280  fundmen  6286  xpsnen  6295  xpcomco  6300  xpdom2  6305  nq0m0r  6552  addpinq1  6560  genipv  6605  genpelvl  6608  genpelvu  6609  cauappcvgprlem1  6755  caucvgsrlemoffres  6882  addresr  6911  mulresr  6912  axcnre  6953  add20  7467  rimul  7574  rereim  7575  mulreim  7593  div4p1lem1div2  8175  nnm1nn0  8221  znegcl  8274  peano2z  8279  nneoor  8338  nn0ind-raph  8353  xnegneg  8744  xltnegi  8746  fzo0to2pr  9072  fldiv4p1lem1div2  9145  frecfzennn  9177  exp0  9233  expp1  9236  expnegap0  9237  1exp  9258  mulexp  9268  sq0i  9319  bernneq  9343  imre  9425  reim0b  9436  rereb  9437  resqrexlemover  9582  resqrexlemcalc1  9586  abs00bd  9638  climconst  9785  ex-ceil  9870  bj-intexr  10002
  Copyright terms: Public domain W3C validator