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  2114  disjiun  3892  euotd  4144  onsucelsucr  4392  isotr  5683  spc2ed  6096  ltbtwnnqq  7187  genpcdl  7291  genpcuu  7292  un0addcl  8964  un0mulcl  8965  btwnnz  9099  uznfz  9834  elfz0ubfz0  9853  fzoss1  9899  elfzo0z  9912  fzofzim  9916  elfzom1p1elfzo  9942  ssfzo12bi  9953  subfzo0  9970  modfzo0difsn  10119  expaddzap  10288  caucvgre  10704  caubnd2  10840  summodc  11103  fzo0dvdseq  11462  nno  11510  lcmdvds  11667  hashgcdeq  11810  neii1  12222  neii2  12224  fsumcncntop  12631
  Copyright terms: Public domain W3C validator