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

Theorem simpl1 893
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
Assertion
Ref Expression
simpl1 (((φ ψ χ) θ) → φ)

Proof of Theorem simpl1
StepHypRef Expression
1 simp1 890 . 2 ((φ ψ χ) → φ)
21adantr 261 1 (((φ ψ χ) θ) → φ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   w3a 871
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100
This theorem depends on definitions:  df-bi 110  df-3an 873
This theorem is referenced by:  simpll1  929  simprl1  935  simp1l1  983  simp2l1  989  simp3l1  995  3anandirs  1221  rspc3ev  2639  brcogw  4427  cocan1  5348  oawordi  5960  nnmord  5997  nnmword  5998  enq0tr  6283  distrlem4prl  6417  distrlem4pru  6418  ltaprg  6449  lelttr  6698  readdcan  6740  addcan  6778  addcan2  6779  ltadd2  7002
  Copyright terms: Public domain W3C validator