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

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

Proof of Theorem simp1l
StepHypRef Expression
1 simpl 108 . 2  |-  ( (
ph  /\  ps )  ->  ph )
213ad2ant1 1003 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 965
This theorem is referenced by:  simpl1l  1033  simpr1l  1039  simp11l  1093  simp21l  1099  simp31l  1105  en2lp  4476  tfisi  4508  funprg  5180  nnsucsssuc  6395  ecopovtrn  6533  ecopovtrng  6536  addassnqg  7213  distrnqg  7218  ltsonq  7229  ltanqg  7231  ltmnqg  7232  distrnq0  7290  addassnq0  7293  mulasssrg  7589  distrsrg  7590  lttrsr  7593  ltsosr  7595  ltasrg  7601  mulextsr1lem  7611  mulextsr1  7612  axmulass  7704  axdistr  7705  dmdcanap  8505  lt2msq1  8666  ltdiv2  8668  lediv2  8672  xaddass  9681  xaddass2  9682  xlt2add  9692  modqdi  10195  expaddzaplem  10366  expaddzap  10367  expmulzap  10369  resqrtcl  10832  bdtrilem  11041  bdtri  11042  xrbdtri  11076  prmexpb  11863  cnptoprest  12445  ssblps  12631  ssbl  12632  rplogbchbase  13073  rplogbreexp  13076  relogbcxpbap  13088
  Copyright terms: Public domain W3C validator