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

Theorem simp1r 1007
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 1003 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 963
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 965
This theorem is referenced by:  simpl1r  1034  simpr1r  1040  simp11r  1094  simp21r  1100  simp31r  1106  vtoclgft  2762  en2lp  4513  funprg  5220  nnsucsssuc  6439  ecopovtrn  6577  ecopovtrng  6580  addassnqg  7302  distrnqg  7307  ltsonq  7318  ltanqg  7320  ltmnqg  7321  distrnq0  7379  addassnq0  7382  prarloclem5  7420  recexprlem1ssl  7553  recexprlem1ssu  7554  mulasssrg  7678  distrsrg  7679  lttrsr  7682  ltsosr  7684  ltasrg  7690  mulextsr1lem  7700  mulextsr1  7701  axmulass  7793  axdistr  7794  dmdcanap  8595  lt2msq1  8756  lediv2  8762  xaddass2  9774  xlt2add  9784  modqdi  10291  expaddzaplem  10462  expaddzap  10463  expmulzap  10465  bdtrilem  11138  xrbdtri  11173  prmexpb  12026  cnptoprest  12650  ssblps  12836  ssbl  12837  rplogbchbase  13278  rplogbreexp  13281  relogbcxpbap  13293
  Copyright terms: Public domain W3C validator