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

Theorem impancom 256
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 113 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32com23 77 . 2  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
43imp 122 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-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  eqrdav  2087  disjiun  3840  euotd  4081  onsucelsucr  4325  isotr  5595  spc2ed  5998  ltbtwnnqq  6972  genpcdl  7076  genpcuu  7077  un0addcl  8704  un0mulcl  8705  btwnnz  8838  uznfz  9513  elfz0ubfz0  9532  fzoss1  9578  elfzo0z  9591  fzofzim  9595  elfzom1p1elfzo  9621  ssfzo12bi  9632  subfzo0  9649  modfzo0difsn  9798  expaddzap  9995  caucvgre  10410  caubnd2  10546  isummo  10769  fzo0dvdseq  11132  nno  11180  lcmdvds  11335  hashgcdeq  11478
  Copyright terms: Public domain W3C validator