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

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

Proof of Theorem simp2l
StepHypRef Expression
1 simpl 107 . 2 ((𝜓𝜒) → 𝜓)
213ad2ant2 961 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  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  simpl2l  992  simpr2l  998  simp12l  1052  simp22l  1058  simp32l  1064  issod  4082  funprg  4980  fsnunf  5394  f1oiso2  5497  ecopovtrn  6269  ecopovtrng  6272  addassnqg  6634  ltsonq  6650  ltanqg  6652  ltmnqg  6653  addassnq0  6714  recexprlem1ssu  6886  mulasssrg  6997  distrsrg  6998  lttrsr  7001  ltsosr  7003  ltasrg  7009  mulextsr1lem  7018  mulextsr1  7019  axmulass  7101  axdistr  7102  dmdcanap  7877  ltdiv2  8032  lediv2  8036  ltdiv23  8037  lediv23  8038  expaddzaplem  9616  expaddzap  9617  expmulzap  9619  expdivap  9624  prmexpb  10674
  Copyright terms: Public domain W3C validator