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

Theorem expcomd 1371
Description: Deduction form of expcom 114. (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 254 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32com23 77 1  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106
This theorem is referenced by:  simplbi2comg  1373  2moswapdc  2032  indifdir  3227  reupick  3255  trintssmOLD  3900  issod  4082  poxp  5884  smores2  5943  smoiun  5950  f1dmvrnfibi  6452  recexprlemm  6876  ltleletr  7260  fzind  8543  iccid  9024  ssfzo12bi  9311  dvdsabseq  10392  divalgb  10469  cncongr1  10629
  Copyright terms: Public domain W3C validator