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

Theorem 3simpc 914
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Andrew Salmon, 13-May-2011.)
Assertion
Ref Expression
3simpc  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ps  /\  ch ) )

Proof of Theorem 3simpc
StepHypRef Expression
1 3anrot 901 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ch  /\ 
ph ) )
2 3simpa 912 . 2  |-  ( ( ps  /\  ch  /\  ph )  ->  ( ps  /\ 
ch ) )
31, 2sylbi 118 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ps  /\  ch ) )
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:  simp3  917  3adant1  933  3adantl1  1071  3adantr1  1074  eupickb  1997  find  4350  eqsupti  6402  divcanap2  7733  diveqap0  7735  divrecap  7741  divcanap3  7749  eliooord  8898  fzrev3  9051  sqdivap  9484  muldvds2  10133  dvdscmul  10134  dvdsmulc  10135  dvdstr  10144
  Copyright terms: Public domain W3C validator