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

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

Proof of Theorem simpl2
StepHypRef Expression
1 simp2 982 . 2 ((𝜑𝜓𝜒) → 𝜓)
21adantr 274 1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 962
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 964
This theorem is referenced by:  simpll2  1021  simprl2  1027  simp1l2  1075  simp2l2  1081  simp3l2  1087  3anandirs  1326  rspc3ev  2806  tfisi  4501  brcogw  4708  oawordi  6365  nnmord  6413  nnmword  6414  ac6sfi  6792  unsnfi  6807  unsnfidcel  6809  ordiso2  6920  prarloclemarch2  7239  enq0tr  7254  distrlem4prl  7404  distrlem4pru  7405  ltaprg  7439  aptiprlemu  7460  lelttr  7864  ltletr  7865  readdcan  7914  addcan  7954  addcan2  7955  ltadd2  8193  ltmul1a  8365  ltmul1  8366  divmulassap  8467  divmulasscomap  8468  lemul1a  8628  xrlelttr  9601  xrltletr  9602  xaddass  9664  xleadd1a  9668  xltadd1  9671  xlesubadd  9678  ixxdisj  9698  icoshftf1o  9786  icodisj  9787  lincmb01cmp  9798  iccf1o  9799  fztri3or  9831  ioom  10050  modqmuladdim  10152  modqmuladdnn0  10153  q2submod  10170  modqaddmulmod  10176  exp3val  10307  ltexp2a  10357  exple1  10361  expnbnd  10427  expnlbnd2  10429  expcan  10475  fiprsshashgt1  10575  maxleastb  10998  maxltsup  11002  xrltmaxsup  11038  xrmaxltsup  11039  xrmaxaddlem  11041  xrmaxadd  11042  addcn2  11091  mulcn2  11093  geoisum1c  11301  dvdsval2  11507  dvdsadd2b  11551  dvdsmod  11571  oexpneg  11585  divalglemex  11630  divalg  11632  gcdass  11714  rplpwr  11726  rppwr  11727  lcmass  11777  coprmdvds2  11785  rpmulgcd2  11787  rpdvds  11791  cncongr2  11796  rpexp  11842  znege1  11867  hashgcdlem  11914  ctinf  11954  topssnei  12345  cnptopco  12405  cnconst2  12416  cnptoprest  12422  cnpdis  12425  upxp  12455  bldisj  12584  blgt0  12585  bl2in  12586  blss2ps  12589  blss2  12590  xblm  12600  blssps  12610  blss  12611  xmetresbl  12623  bdbl  12686  bdmopn  12687  metcnp3  12694  metcnp  12695  metcnp2  12696  dvfvalap  12833  dvcnp2cntop  12846  dvcn  12847  logdivlti  12981
  Copyright terms: Public domain W3C validator