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  2081  euotd  4017  onsucelsucr  4260  isotr  5487  spc2ed  5885  ltbtwnnqq  6667  genpcdl  6771  genpcuu  6772  un0addcl  8388  un0mulcl  8389  btwnnz  8522  uznfz  9196  elfz0ubfz0  9213  fzoss1  9257  elfzo0z  9270  fzofzim  9274  elfzom1p1elfzo  9300  ssfzo12bi  9311  subfzo0  9328  modfzo0difsn  9477  expaddzap  9617  caucvgre  10005  caubnd2  10141  fzo0dvdseq  10402  nno  10450  lcmdvds  10605
  Copyright terms: Public domain W3C validator