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

Theorem expcomd 1441
Description: Deduction form of expcom 116. (Contributed by Alan Sare, 22-Jul-2012.)
Hypothesis
Ref Expression
expcomd.1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
expcomd  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )

Proof of Theorem expcomd
StepHypRef Expression
1 expcomd.1 . . 3  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
21expd 258 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32com23 78 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-ia3 108
This theorem is referenced by:  simplbi2comg  1443  2moswapdc  2116  indifdir  3391  reupick  3419  issod  4319  poxp  6232  smores2  6294  smoiun  6301  mapxpen  6847  f1dmvrnfibi  6942  recexprlemm  7622  ltleletr  8037  fzind  9366  iccid  9923  ssfzo12bi  10222  dvdsabseq  11847  divalgb  11924  cncongr1  12097  difsqpwdvds  12331  txlm  13672  blsscls2  13886  metcnpi3  13910
  Copyright terms: Public domain W3C validator