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

Theorem 3simpc 963
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 950 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ch  /\ 
ph ) )
2 3simpa 961 . 2  |-  ( ( ps  /\  ch  /\  ph )  ->  ( ps  /\ 
ch ) )
31, 2sylbi 120 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ps  /\  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 945
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 947
This theorem is referenced by:  simp3  966  3adant1  982  3adantl1  1120  3adantr1  1123  eupickb  2056  find  4481  fisseneq  6786  eqsupti  6849  divcanap2  8403  diveqap0  8405  divrecap  8411  divcanap3  8421  eliooord  9662  fzrev3  9818  sqdivap  10308  muldvds2  11426  dvdscmul  11427  dvdsmulc  11428  dvdstr  11437  cncfmptc  12657  cnplimclemr  12713
  Copyright terms: Public domain W3C validator