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

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

Proof of Theorem simp1r
StepHypRef Expression
1 simpr 107 . 2  |-  ( (
ph  /\  ps )  ->  ps )
213ad2ant1 936 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
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:  simpl1r  967  simpr1r  973  simp11r  1027  simp21r  1033  simp31r  1039  vtoclgft  2621  en2lp  4306  funprg  4977  nnsucsssuc  6102  ecopovtrn  6234  ecopovtrng  6237  addassnqg  6538  distrnqg  6543  ltsonq  6554  ltanqg  6556  ltmnqg  6557  distrnq0  6615  addassnq0  6618  prarloclem5  6656  recexprlem1ssl  6789  recexprlem1ssu  6790  mulasssrg  6901  distrsrg  6902  lttrsr  6905  ltsosr  6907  ltasrg  6913  mulextsr1lem  6922  mulextsr1  6923  axmulass  7005  axdistr  7006  dmdcanap  7773  lt2msq1  7926  lediv2  7932  modqdi  9342  expaddzaplem  9463  expaddzap  9464  expmulzap  9466
  Copyright terms: Public domain W3C validator