ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3simpa Structured version   Unicode version

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

Proof of Theorem 3simpa
StepHypRef Expression
1 df-3an 886 . 2
21simplbi 259 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   w3a 884
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110  df-3an 886
This theorem is referenced by:  3simpb  901  3simpc  902  simp1  903  simp2  904  3adant3  923  3adantl3  1061  3adantr3  1064  opprc  3561  oprcl  3564  opm  3962  funtpg  4893  ftpg  5290  ovig  5564  prltlu  6470  mullocpr  6552  lt2halves  7937  nn0n0n1ge2  8087  ixxssixx  8541  bj-peano4  9415
  Copyright terms: Public domain W3C validator