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

Theorem ancomsd 260
Description: Deduction commuting conjunction in antecedent. (Contributed by NM, 12-Dec-2004.)
Hypothesis
Ref Expression
ancomsd.1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
ancomsd  |-  ( ph  ->  ( ( ch  /\  ps )  ->  th )
)

Proof of Theorem ancomsd
StepHypRef Expression
1 ancom 257 . 2  |-  ( ( ch  /\  ps )  <->  ( ps  /\  ch )
)
2 ancomsd.1 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
31, 2syl5bi 145 1  |-  ( ph  ->  ( ( ch  /\  ps )  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
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
This theorem is referenced by:  sylan2d  282  mpand  413  anabsi6  522  ralxfrd  4222  rexxfrd  4223  poirr2  4745  smoel  5946  genprndl  6677  genprndu  6678  addcanprlemu  6771  leltadd  7516  lemul12b  7902  lbzbi  8648  dvdssub2  10149
  Copyright terms: Public domain W3C validator