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

Theorem expcomd 1400
Description: Deduction form of expcom 115. (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 256 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32com23 78 1  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107
This theorem is referenced by:  simplbi2comg  1402  2moswapdc  2065  indifdir  3300  reupick  3328  issod  4209  poxp  6095  smores2  6157  smoiun  6164  mapxpen  6708  f1dmvrnfibi  6798  recexprlemm  7396  ltleletr  7810  fzind  9120  iccid  9659  ssfzo12bi  9953  dvdsabseq  11452  divalgb  11529  cncongr1  11691  txlm  12354  blsscls2  12568  metcnpi3  12592
  Copyright terms: Public domain W3C validator