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  2663  tfisi  4297  brcogw  4491  oawordi  6036  nnmord  6077  nnmword  6078  ac6sfi  6338  prarloclemarch2  6498  enq0tr  6513  distrlem4prl  6663  distrlem4pru  6664  ltaprg  6698  aptiprlemu  6719  lelttr  7086  ltletr  7087  readdcan  7133  addcan  7171  addcan2  7172  ltadd2  7395  ltmul1a  7558  ltmul1  7559  lemul1a  7800  xrlelttr  8689  xrltletr  8690  ixxdisj  8739  icoshftf1o  8826  icodisj  8827  lincmb01cmp  8838  iccf1o  8839  fztri3or  8870  ltexp2a  9184  exple1  9188  expnbnd  9250  expnlbnd2  9252  addcn2  9708  mulcn2  9710
  Copyright terms: Public domain W3C validator