NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  simp1 Unicode version

Theorem simp1 955
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
Assertion
Ref Expression
simp1

Proof of Theorem simp1
StepHypRef Expression
1 3simpa 952 . 2
21simpld 445 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   w3a 934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
This theorem is referenced by:  simpl1  958  simpr1  961  simp1i  964  simp1d  967  simp11  985  simp21  988  simp31  991  syld3an3  1227  rsp2e  2677  opkthg  4131  ltfintri  4466  ssfin  4470  foco2  5426  f1oiso2  5500  xpassen  6057  enadj  6060  lectr  6211
  Copyright terms: Public domain W3C validator