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

Theorem impancom 247
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 108 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32com23 72 . 2  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
43imp 115 1  |-  ( (
ph  /\  ch )  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  eqrdav  2039  euotd  3988  onsucelsucr  4230  isotr  5443  ltbtwnnqq  6494  genpcdl  6598  genpcuu  6599  un0addcl  8187  un0mulcl  8188  btwnnz  8306  uznfz  8932  elfz0ubfz0  8949  fzoss1  8994  elfzo0z  9007  fzofzim  9011  elfzom1p1elfzo  9037  ssfzo12bi  9048  expaddzap  9177  caucvgre  9458  caubnd2  9591
  Copyright terms: Public domain W3C validator