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

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

Proof of Theorem simpl2
StepHypRef Expression
1 simp2 905 . 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:  simpll2  944  simprl2  950  simp1l2  998  simp2l2  1004  simp3l2  1010  3anandirs  1238  rspc3ev  2666  tfisi  4310  brcogw  4504  oawordi  6049  nnmord  6090  nnmword  6091  ac6sfi  6352  ordiso2  6355  prarloclemarch2  6515  enq0tr  6530  distrlem4prl  6680  distrlem4pru  6681  ltaprg  6715  aptiprlemu  6736  lelttr  7104  ltletr  7105  readdcan  7151  addcan  7189  addcan2  7190  ltadd2  7414  ltmul1a  7580  ltmul1  7581  lemul1a  7822  xrlelttr  8720  xrltletr  8721  ixxdisj  8770  icoshftf1o  8857  icodisj  8858  lincmb01cmp  8869  iccf1o  8870  fztri3or  8901  ltexp2a  9280  exple1  9284  expnbnd  9346  expnlbnd2  9348  addcn2  9804  mulcn2  9806
  Copyright terms: Public domain W3C validator