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

Theorem expcomd 1486
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  1488  2moswapdc  2170  indifdir  3463  reupick  3491  issod  4416  poxp  6397  smores2  6460  smoiun  6467  mapxpen  7034  f1dmvrnfibi  7143  recexprlemm  7844  ltleletr  8261  fzind  9595  iccid  10160  ssfzo12bi  10471  pfxccatin12lem2  11316  swrdccat  11320  dvdsabseq  12413  divalgb  12491  cncongr1  12680  difsqpwdvds  12916  lss1d  14403  txlm  15009  blsscls2  15223  metcnpi3  15247  clwwlknonex2lem2  16295
  Copyright terms: Public domain W3C validator