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

Theorem simp1l 939
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 106 . 2  |-  ( (
ph  /\  ps )  ->  ph )
213ad2ant1 936 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
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:  simpl1l  966  simpr1l  972  simp11l  1026  simp21l  1032  simp31l  1038  en2lp  4306  tfisi  4338  funprg  4977  nnsucsssuc  6102  ecopovtrn  6234  ecopovtrng  6237  addassnqg  6538  distrnqg  6543  ltsonq  6554  ltanqg  6556  ltmnqg  6557  distrnq0  6615  addassnq0  6618  mulasssrg  6901  distrsrg  6902  lttrsr  6905  ltsosr  6907  ltasrg  6913  mulextsr1lem  6922  mulextsr1  6923  axmulass  7005  axdistr  7006  dmdcanap  7773  lt2msq1  7926  ltdiv2  7928  lediv2  7932  modqdi  9342  expaddzaplem  9463  expaddzap  9464  expmulzap  9466  resqrtcl  9856
  Copyright terms: Public domain W3C validator