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

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

Proof of Theorem simpl1
StepHypRef Expression
1 simp1 939 . 2 ((𝜑𝜓𝜒) → 𝜑)
21adantr 270 1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  simpll1  978  simprl1  984  simp1l1  1032  simp2l1  1038  simp3l1  1044  3anandirs  1280  rspc3ev  2718  brcogw  4526  cocan1  5452  oawordi  6107  nnmord  6149  nnmword  6150  dif1en  6404  ac6sfi  6421  ordiso2  6495  enq0tr  6675  distrlem4prl  6825  distrlem4pru  6826  ltaprg  6860  aptiprlemu  6881  lelttr  7255  readdcan  7304  addcan  7344  addcan2  7345  ltadd2  7579  ltmul1a  7747  ltmul1  7748  divmulassap  7839  divmulasscomap  7840  lemul1a  7992  xrlelttr  8941  icoshftf1o  9078  lincmb01cmp  9090  iccf1o  9091  fztri3or  9123  fzofzim  9263  ioom  9336  modqmuladdim  9438  modqm1p1mod0  9446  q2submod  9456  modqaddmulmod  9462  ltexp2a  9614  exple1  9618  expnlbnd2  9684  expcan  9730  maxleastb  10227  maxltsup  10231  addcn2  10276  mulcn2  10278  dvdsadd2b  10376  dvdsmod  10396  oexpneg  10410  divalglemex  10455  divalg  10457  gcdass  10537  rplpwr  10549  rppwr  10550  coprmdvds2  10608  rpmulgcd2  10610  qredeq  10611  rpdvds  10614  cncongr2  10619  rpexp  10665  znege1  10689
  Copyright terms: Public domain W3C validator