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

Theorem simp2l 1007
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp2l ((𝜑 ∧ (𝜓𝜒) ∧ 𝜃) → 𝜓)

Proof of Theorem simp2l
StepHypRef Expression
1 simpl 108 . 2 ((𝜓𝜒) → 𝜓)
213ad2ant2 1003 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  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 964
This theorem is referenced by:  simpl2l  1034  simpr2l  1040  simp12l  1094  simp22l  1100  simp32l  1106  issod  4241  funprg  5173  fsnunf  5620  f1oiso2  5728  ecopovtrn  6526  ecopovtrng  6529  addassnqg  7202  ltsonq  7218  ltanqg  7220  ltmnqg  7221  addassnq0  7282  recexprlem1ssu  7454  mulasssrg  7578  distrsrg  7579  lttrsr  7582  ltsosr  7584  ltasrg  7590  mulextsr1lem  7600  mulextsr1  7601  axmulass  7693  axdistr  7694  dmdcanap  8494  ltdiv2  8657  lediv2  8661  ltdiv23  8662  lediv23  8663  xaddass  9664  xaddass2  9665  xlt2add  9675  expaddzaplem  10348  expaddzap  10349  expmulzap  10351  expdivap  10356  leisorel  10592  bdtrilem  11022  bdtri  11023  xrbdtri  11057  fsumsplitsnun  11200  prmexpb  11840  cnptoprest  12422  ssblps  12608  ssbl  12609  tgqioo  12730
  Copyright terms: Public domain W3C validator