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

Theorem imp31 256
Description: An importation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
imp3.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
imp31  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )

Proof of Theorem imp31
StepHypRef Expression
1 imp3.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
21imp 124 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
32imp 124 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107
This theorem is referenced by:  imp41  353  imp5d  359  impl  380  anassrs  400  an31s  570  con4biddc  857  3imp  1193  3expa  1203  bilukdc  1396  reusv3  4460  dfimafn  5564  funimass4  5566  funimass3  5632  isopolem  5822  smores2  6294  tfrlem9  6319  nnmordi  6516  mulcanpig  7333  elnnz  9262  nzadd  9304  irradd  9645  irrmul  9646  uzsubsubfz  10046  fzo1fzo0n0  10182  elfzonelfzo  10229  infpnlem1  12356  tgcl  13534
  Copyright terms: Public domain W3C validator