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

Theorem simp1r 1017
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 109 . 2  |-  ( (
ph  /\  ps )  ->  ps )
213ad2ant1 1013 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 975
This theorem is referenced by:  simpl1r  1044  simpr1r  1050  simp11r  1104  simp21r  1110  simp31r  1116  vtoclgft  2780  en2lp  4538  funprg  5248  nnsucsssuc  6471  ecopovtrn  6610  ecopovtrng  6613  addassnqg  7344  distrnqg  7349  ltsonq  7360  ltanqg  7362  ltmnqg  7363  distrnq0  7421  addassnq0  7424  prarloclem5  7462  recexprlem1ssl  7595  recexprlem1ssu  7596  mulasssrg  7720  distrsrg  7721  lttrsr  7724  ltsosr  7726  ltasrg  7732  mulextsr1lem  7742  mulextsr1  7743  axmulass  7835  axdistr  7836  dmdcanap  8639  lt2msq1  8801  lediv2  8807  xaddass2  9827  xlt2add  9837  modqdi  10348  expaddzaplem  10519  expaddzap  10520  expmulzap  10522  bdtrilem  11202  xrbdtri  11239  prmexpb  12105  mgmsscl  12615  cnptoprest  13033  ssblps  13219  ssbl  13220  rplogbchbase  13662  rplogbreexp  13665  relogbcxpbap  13677  lgssq  13735
  Copyright terms: Public domain W3C validator