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

Theorem simp3l 943
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp3l  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  ch )

Proof of Theorem simp3l
StepHypRef Expression
1 simpl 106 . 2  |-  ( ( ch  /\  th )  ->  ch )
213ad2ant3 938 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    /\ w3a 896
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 898
This theorem is referenced by:  simpl3l  970  simpr3l  976  simp13l  1030  simp23l  1036  simp33l  1042  issod  4084  tfisi  4338  tfrlem5  5961  tfrlemibxssdm  5972  ecopovtrn  6234  ecopovtrng  6237  addassnqg  6538  ltsonq  6554  ltanqg  6556  ltmnqg  6557  addassnq0  6618  mulasssrg  6901  distrsrg  6902  lttrsr  6905  ltsosr  6907  ltasrg  6913  mulextsr1lem  6922  mulextsr1  6923  axmulass  7005  axdistr  7006  lemul1  7658  reapmul1lem  7659  reapmul1  7660  mulcanap  7720  mulcanap2  7721  divassap  7743  divdirap  7748  div11ap  7751  muldivdirap  7758  divcanap5  7765  apmul1  7839  ltdiv1  7909  ltmuldiv  7915  ledivmul  7918  lemuldiv  7922  ltdiv2  7928  lediv2  7932  ltdiv23  7933  lediv23  7934  modqdi  9342  expaddzap  9464  expmulzap  9466  resqrtcl  9856  dvdscmulr  10136  dvdsmulcr  10137  dvdsadd2b  10154
  Copyright terms: Public domain W3C validator