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

Theorem simp1l 967
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 107 . 2  |-  ( (
ph  /\  ps )  ->  ph )
213ad2ant1 964 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    /\ w3a 924
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 926
This theorem is referenced by:  simpl1l  994  simpr1l  1000  simp11l  1054  simp21l  1060  simp31l  1066  en2lp  4370  tfisi  4402  funprg  5064  nnsucsssuc  6253  ecopovtrn  6387  ecopovtrng  6390  addassnqg  6939  distrnqg  6944  ltsonq  6955  ltanqg  6957  ltmnqg  6958  distrnq0  7016  addassnq0  7019  mulasssrg  7302  distrsrg  7303  lttrsr  7306  ltsosr  7308  ltasrg  7314  mulextsr1lem  7323  mulextsr1  7324  axmulass  7406  axdistr  7407  dmdcanap  8187  lt2msq1  8344  ltdiv2  8346  lediv2  8350  modqdi  9795  expaddzaplem  9994  expaddzap  9995  expmulzap  9997  resqrtcl  10458  prmexpb  11404
  Copyright terms: Public domain W3C validator