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

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

Proof of Theorem simpl2
StepHypRef Expression
1 simp2 904 . 2 ((φ ψ χ) → ψ)
21adantr 261 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  ax-ia2 100
This theorem depends on definitions:  df-bi 110  df-3an 886
This theorem is referenced by:  simpll2  943  simprl2  949  simp1l2  997  simp2l2  1003  simp3l2  1009  3anandirs  1237  rspc3ev  2660  tfisi  4253  brcogw  4447  oawordi  5988  nnmord  6026  nnmword  6027  prarloclemarch2  6402  enq0tr  6416  distrlem4prl  6559  distrlem4pru  6560  ltaprg  6591  aptiprlemu  6611  lelttr  6883  ltletr  6884  readdcan  6930  addcan  6968  addcan2  6969  ltadd2  7192  ltmul1a  7355  ltmul1  7356  lemul1a  7585  xrlelttr  8472  xrltletr  8473  ixxdisj  8522  icoshftf1o  8609  icodisj  8610  lincmb01cmp  8621  iccf1o  8622  fztri3or  8653  ltexp2a  8940  exple1  8944  expnbnd  9005  expnlbnd2  9007
  Copyright terms: Public domain W3C validator