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

Theorem simp2l 967
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 963 1 ((𝜑 ∧ (𝜓𝜒) ∧ 𝜃) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 922
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 924
This theorem is referenced by:  simpl2l  994  simpr2l  1000  simp12l  1054  simp22l  1060  simp32l  1066  issod  4120  funprg  5029  fsnunf  5459  f1oiso2  5567  ecopovtrn  6341  ecopovtrng  6344  addassnqg  6885  ltsonq  6901  ltanqg  6903  ltmnqg  6904  addassnq0  6965  recexprlem1ssu  7137  mulasssrg  7248  distrsrg  7249  lttrsr  7252  ltsosr  7254  ltasrg  7260  mulextsr1lem  7269  mulextsr1  7270  axmulass  7352  axdistr  7353  dmdcanap  8128  ltdiv2  8283  lediv2  8287  ltdiv23  8288  lediv23  8289  expaddzaplem  9897  expaddzap  9898  expmulzap  9900  expdivap  9905  leisorel  10139  prmexpb  11012
  Copyright terms: Public domain W3C validator