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

Theorem simpl1 907
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
Assertion
Ref Expression
simpl1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜑)

Proof of Theorem simpl1
StepHypRef Expression
1 simp1 904 . 2 ((𝜑𝜓𝜒) → 𝜑)
21adantr 261 1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  w3a 885
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 887
This theorem is referenced by:  simpll1  943  simprl1  949  simp1l1  997  simp2l1  1003  simp3l1  1009  3anandirs  1238  rspc3ev  2666  brcogw  4504  cocan1  5427  oawordi  6049  nnmord  6090  nnmword  6091  dif1en  6337  ac6sfi  6352  ordiso2  6355  enq0tr  6530  distrlem4prl  6680  distrlem4pru  6681  ltaprg  6715  aptiprlemu  6736  lelttr  7104  readdcan  7151  addcan  7189  addcan2  7190  ltadd2  7414  ltmul1a  7580  ltmul1  7581  lemul1a  7822  xrlelttr  8720  icoshftf1o  8857  lincmb01cmp  8869  iccf1o  8870  fztri3or  8901  fzofzim  9042  ltexp2a  9304  exple1  9308  expnlbnd2  9372  addcn2  9829  mulcn2  9831
  Copyright terms: Public domain W3C validator