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  6357  enq0tr  6532  distrlem4prl  6682  distrlem4pru  6683  ltaprg  6717  aptiprlemu  6738  lelttr  7106  readdcan  7153  addcan  7191  addcan2  7192  ltadd2  7416  ltmul1a  7582  ltmul1  7583  lemul1a  7824  xrlelttr  8722  icoshftf1o  8859  lincmb01cmp  8871  iccf1o  8872  fztri3or  8903  fzofzim  9044  ltexp2a  9306  exple1  9310  expnlbnd2  9374  addcn2  9831  mulcn2  9833
  Copyright terms: Public domain W3C validator