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

Theorem imp31 252
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 122 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
32imp 122 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  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
This theorem is referenced by:  imp41  345  imp5d  351  impl  372  anassrs  392  an31s  535  con4biddc  788  3imp  1133  3expa  1139  bilukdc  1328  reusv3  4218  dfimafn  5254  funimass4  5256  funimass3  5315  isopolem  5492  smores2  5943  tfrlem9  5968  nnmordi  6155  mulcanpig  6587  elnnz  8442  nzadd  8484  irradd  8812  irrmul  8813  uzsubsubfz  9142  fzo1fzo0n0  9269  elfzonelfzo  9316
  Copyright terms: Public domain W3C validator