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

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

Proof of Theorem simp2l
StepHypRef Expression
1 simpl 106 . 2 ((𝜓𝜒) → 𝜓)
213ad2ant2 935 1 ((𝜑 ∧ (𝜓𝜒) ∧ 𝜃) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  w3a 894
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 896
This theorem is referenced by:  simpl2l  966  simpr2l  972  simp12l  1026  simp22l  1032  simp32l  1038  issod  4081  funprg  4974  fsnunf  5387  f1oiso2  5491  ecopovtrn  6231  ecopovtrng  6234  addassnqg  6508  ltsonq  6524  ltanqg  6526  ltmnqg  6527  addassnq0  6588  recexprlem1ssu  6760  mulasssrg  6871  distrsrg  6872  lttrsr  6875  ltsosr  6877  ltasrg  6883  mulextsr1lem  6892  mulextsr1  6893  axmulass  6975  axdistr  6976  dmdcanap  7743  ltdiv2  7898  lediv2  7902  ltdiv23  7903  lediv23  7904  expaddzaplem  9428  expaddzap  9429  expmulzap  9431  expdivap  9436
  Copyright terms: Public domain W3C validator