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

Theorem simp2l 975
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 971 1 ((𝜑 ∧ (𝜓𝜒) ∧ 𝜃) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 930
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 932
This theorem is referenced by:  simpl2l  1002  simpr2l  1008  simp12l  1062  simp22l  1068  simp32l  1074  issod  4179  funprg  5109  fsnunf  5552  f1oiso2  5660  ecopovtrn  6456  ecopovtrng  6459  addassnqg  7091  ltsonq  7107  ltanqg  7109  ltmnqg  7110  addassnq0  7171  recexprlem1ssu  7343  mulasssrg  7454  distrsrg  7455  lttrsr  7458  ltsosr  7460  ltasrg  7466  mulextsr1lem  7475  mulextsr1  7476  axmulass  7558  axdistr  7559  dmdcanap  8343  ltdiv2  8503  lediv2  8507  ltdiv23  8508  lediv23  8509  xaddass  9493  xaddass2  9494  xlt2add  9504  expaddzaplem  10177  expaddzap  10178  expmulzap  10180  expdivap  10185  leisorel  10421  bdtrilem  10849  bdtri  10850  xrbdtri  10884  fsumsplitsnun  11027  prmexpb  11622  cnptoprest  12189  ssblps  12353  ssbl  12354  tgqioo  12466
  Copyright terms: Public domain W3C validator