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

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

Proof of Theorem simpl2
StepHypRef Expression
1 simp2 916 . 2 ((𝜑𝜓𝜒) → 𝜓)
21adantr 265 1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  simpll2  955  simprl2  961  simp1l2  1009  simp2l2  1015  simp3l2  1021  3anandirs  1254  rspc3ev  2689  tfisi  4338  brcogw  4532  oawordi  6080  nnmord  6121  nnmword  6122  ac6sfi  6383  ordiso2  6415  prarloclemarch2  6575  enq0tr  6590  distrlem4prl  6740  distrlem4pru  6741  ltaprg  6775  aptiprlemu  6796  lelttr  7165  ltletr  7166  readdcan  7214  addcan  7254  addcan2  7255  ltadd2  7488  ltmul1a  7656  ltmul1  7657  lemul1a  7899  xrlelttr  8823  xrltletr  8824  ixxdisj  8873  icoshftf1o  8960  icodisj  8961  lincmb01cmp  8972  iccf1o  8973  fztri3or  9005  ioom  9217  modqmuladdim  9317  modqmuladdnn0  9318  q2submod  9335  modqaddmulmod  9341  ltexp2a  9472  exple1  9476  expnbnd  9540  expnlbnd2  9542  addcn2  10062  mulcn2  10064  dvdsval2  10111  dvdsadd2b  10154  dvdsmod  10174  oexpneg  10188  divalglemex  10234  divalg  10236
  Copyright terms: Public domain W3C validator