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

Theorem impancom 258
Description: Mixed importation/commutation inference. (Contributed by NM, 22-Jun-2013.)
Hypothesis
Ref Expression
impancom.1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Assertion
Ref Expression
impancom  |-  ( (
ph  /\  ch )  ->  ( ps  ->  th )
)

Proof of Theorem impancom
StepHypRef Expression
1 impancom.1 . . . 4  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
21ex 114 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32com23 78 . 2  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
43imp 123 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-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  eqrdav  2169  disjiun  3984  euotd  4239  onsucelsucr  4492  isotr  5795  spc2ed  6212  ltbtwnnqq  7377  genpcdl  7481  genpcuu  7482  un0addcl  9168  un0mulcl  9169  btwnnz  9306  uznfz  10059  elfz0ubfz0  10081  fzoss1  10127  elfzo0z  10140  fzofzim  10144  elfzom1p1elfzo  10170  ssfzo12bi  10181  subfzo0  10198  modfzo0difsn  10351  expaddzap  10520  caucvgre  10945  caubnd2  11081  summodc  11346  fzo0dvdseq  11817  nno  11865  lcmdvds  12033  hashgcdeq  12193  modprm0  12208  pcqcl  12260  neii1  12941  neii2  12943  fsumcncntop  13350
  Copyright terms: Public domain W3C validator