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

Theorem simp1l 928
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 102 . 2  |-  ( (
ph  /\  ps )  ->  ph )
213ad2ant1 925 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97    /\ w3a 885
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-3an 887
This theorem is referenced by:  simpl1l  955  simpr1l  961  simp11l  1015  simp21l  1021  simp31l  1027  en2lp  4278  tfisi  4310  funprg  4949  nnsucsssuc  6071  ecopovtrn  6203  ecopovtrng  6206  addassnqg  6480  distrnqg  6485  ltsonq  6496  ltanqg  6498  ltmnqg  6499  distrnq0  6557  addassnq0  6560  mulasssrg  6843  distrsrg  6844  lttrsr  6847  ltsosr  6849  ltasrg  6855  mulextsr1lem  6864  mulextsr1  6865  axmulass  6947  axdistr  6948  dmdcanap  7698  lt2msq1  7851  ltdiv2  7853  lediv2  7857  expaddzaplem  9298  expaddzap  9299  expmulzap  9301  resqrtcl  9627
  Copyright terms: Public domain W3C validator