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

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

Proof of Theorem simpl2
StepHypRef Expression
1 simp2 891 . 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:  simpll2  930  simprl2  936  simp1l2  984  simp2l2  990  simp3l2  996  3anandirs  1221  rspc3ev  2639  tfisi  4233  brcogw  4427  oawordi  5960  nnmord  5997  nnmword  5998  prarloclemarch2  6270  enq0tr  6283  distrlem4prl  6417  distrlem4pru  6418  ltaprg  6449  lelttr  6698  ltletr  6699  readdcan  6740  addcan  6778  addcan2  6779  ltadd2  7002
  Copyright terms: Public domain W3C validator