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

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

Proof of Theorem simpl1
StepHypRef Expression
1 simp1 903 . 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:  simpll1  942  simprl1  948  simp1l1  996  simp2l1  1002  simp3l1  1008  3anandirs  1237  rspc3ev  2660  brcogw  4447  cocan1  5370  oawordi  5988  nnmord  6026  nnmword  6027  enq0tr  6416  distrlem4prl  6559  distrlem4pru  6560  ltaprg  6591  aptiprlemu  6611  lelttr  6883  readdcan  6930  addcan  6968  addcan2  6969  ltadd2  7192  ltmul1a  7355  ltmul1  7356  lemul1a  7585  xrlelttr  8472  icoshftf1o  8609  lincmb01cmp  8621  iccf1o  8622  fztri3or  8653  fzofzim  8794  ltexp2a  8940  exple1  8944  expnlbnd2  9007
  Copyright terms: Public domain W3C validator