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

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

Proof of Theorem simpl1
StepHypRef Expression
1 simp1 964 . 2 ((𝜑𝜓𝜒) → 𝜑)
21adantr 272 1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  simpll1  1003  simprl1  1009  simp1l1  1057  simp2l1  1063  simp3l1  1069  3anandirs  1309  rspc3ev  2778  brcogw  4676  cocan1  5654  oawordi  6331  nnmord  6379  nnmword  6380  dif1en  6739  ac6sfi  6758  ordiso2  6886  difinfsn  6951  ctssdc  6964  enq0tr  7206  distrlem4prl  7356  distrlem4pru  7357  ltaprg  7391  aptiprlemu  7412  lelttr  7816  readdcan  7866  addcan  7906  addcan2  7907  ltadd2  8145  ltmul1a  8316  ltmul1  8317  divmulassap  8418  divmulasscomap  8419  lemul1a  8576  xrlelttr  9540  xleadd1a  9607  xlesubadd  9617  icoshftf1o  9725  lincmb01cmp  9737  iccf1o  9738  fztri3or  9770  fzofzim  9916  ioom  9989  modqmuladdim  10091  modqm1p1mod0  10099  q2submod  10109  modqaddmulmod  10115  ltexp2a  10296  exple1  10300  expnlbnd2  10368  expcan  10414  fiprsshashgt1  10514  fimaxq  10524  maxleastb  10937  maxltsup  10941  xrltmaxsup  10977  xrmaxltsup  10978  xrmaxaddlem  10980  addcn2  11030  mulcn2  11032  dvdsadd2b  11447  dvdsmod  11467  oexpneg  11481  divalglemex  11526  divalg  11528  gcdass  11610  rplpwr  11622  rppwr  11623  coprmdvds2  11681  rpmulgcd2  11683  qredeq  11684  rpdvds  11687  cncongr2  11692  rpexp  11738  znege1  11762  hashgcdlem  11809  ctinf  11849  neiint  12220  topssnei  12237  iscnp4  12293  cnptopco  12297  cnconst2  12308  cnrest2  12311  cnptoprest  12314  cnpdis  12317  bldisj  12476  blgt0  12477  bl2in  12478  blss2ps  12481  blss2  12482  xblm  12492  blssps  12502  blss  12503  xmetresbl  12515  bdbl  12578  metcnp3  12586  metcnp2  12588  cncfmptc  12657  dvcnp2cntop  12738  dvcn  12739
  Copyright terms: Public domain W3C validator