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

Theorem ancomsd 269
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 266 . 2  |-  ( ( ch  /\  ps )  <->  ( ps  /\  ch )
)
2 ancomsd.1 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
31, 2biimtrid 152 1  |-  ( ph  ->  ( ( ch  /\  ps )  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
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
This theorem is referenced by:  sylan2d  294  mpand  429  anabsi6  580  ralxfrd  4474  rexxfrd  4475  poirr2  5033  smoel  6315  genprndl  7534  genprndu  7535  addcanprlemu  7628  leltadd  8418  lemul12b  8832  lbzbi  9630  dvdssub2  11856  odzdvds  12259
  Copyright terms: Public domain W3C validator