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  3392  reupick  3420  issod  4320  poxp  6233  smores2  6295  smoiun  6302  mapxpen  6848  f1dmvrnfibi  6943  recexprlemm  7623  ltleletr  8039  fzind  9368  iccid  9925  ssfzo12bi  10225  dvdsabseq  11853  divalgb  11930  cncongr1  12103  difsqpwdvds  12337  txlm  13782  blsscls2  13996  metcnpi3  14020
  Copyright terms: Public domain W3C validator