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

Theorem 3simpc 996
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 983 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ch  /\ 
ph ) )
2 3simpa 994 . 2  |-  ( ( ps  /\  ch  /\  ph )  ->  ( ps  /\ 
ch ) )
31, 2sylbi 121 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ps  /\  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    /\ w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  simp3  999  3adant1  1015  3adantl1  1153  3adantr1  1156  eupickb  2107  find  4598  fisseneq  6930  eqsupti  6994  divcanap2  8635  diveqap0  8637  divrecap  8643  divcanap3  8653  eliooord  9926  fzrev3  10084  sqdivap  10581  muldvds2  11819  dvdscmul  11820  dvdsmulc  11821  dvdstr  11830  cncfmptc  13975  cnplimclemr  14031
  Copyright terms: Public domain W3C validator