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

Theorem simp2l 929
 Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp2l ((φ (ψ χ) θ) → ψ)

Proof of Theorem simp2l
StepHypRef Expression
1 simpl 102 . 2 ((ψ χ) → ψ)
213ad2ant2 925 1 ((φ (ψ χ) θ) → ψ)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 884 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110  df-3an 886 This theorem is referenced by:  simpl2l  956  simpr2l  962  simp12l  1016  simp22l  1022  simp32l  1028  issod  4047  funprg  4892  fsnunf  5305  f1oiso2  5409  ecopovtrn  6139  ecopovtrng  6142  addassnqg  6366  ltsonq  6382  ltanqg  6384  ltmnqg  6385  addassnq0  6444  recexprlem1ssu  6605  mulasssrg  6666  distrsrg  6667  lttrsr  6670  ltsosr  6672  ltasrg  6678  mulextsr1lem  6686  mulextsr1  6687  axmulass  6737  axdistr  6738  dmdcanap  7460  ltdiv2  7614  lediv2  7618  ltdiv23  7619  lediv23  7620  expaddzaplem  8932  expaddzap  8933  expmulzap  8935  expdivap  8939
 Copyright terms: Public domain W3C validator