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