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

Theorem simp1r 968
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 108 . 2  |-  ( (
ph  /\  ps )  ->  ps )
213ad2ant1 964 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
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:  simpl1r  995  simpr1r  1001  simp11r  1055  simp21r  1061  simp31r  1067  vtoclgft  2669  en2lp  4370  funprg  5064  nnsucsssuc  6253  ecopovtrn  6389  ecopovtrng  6392  addassnqg  6941  distrnqg  6946  ltsonq  6957  ltanqg  6959  ltmnqg  6960  distrnq0  7018  addassnq0  7021  prarloclem5  7059  recexprlem1ssl  7192  recexprlem1ssu  7193  mulasssrg  7304  distrsrg  7305  lttrsr  7308  ltsosr  7310  ltasrg  7316  mulextsr1lem  7325  mulextsr1  7326  axmulass  7408  axdistr  7409  dmdcanap  8189  lt2msq1  8346  lediv2  8352  modqdi  9799  expaddzaplem  9998  expaddzap  9999  expmulzap  10001  prmexpb  11408
  Copyright terms: Public domain W3C validator