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

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

Proof of Theorem imp32
StepHypRef Expression
1 imp3.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
21impd 254 . 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:  imp42  354  impr  379  anasss  399  an13s  567  3expb  1204  reuss2  3415  reupick  3419  po2nr  4309  fvmptt  5607  fliftfund  5797  f1ocnv2d  6074  addclpi  7325  addnidpig  7334  mulnqprl  7566  mulnqpru  7567  ltsubrp  9688  ltaddrp  9689  divgcdcoprm0  12095  infpnlem1  12351  innei  13594  tgcnp  13640  isxmetd  13778
  Copyright terms: Public domain W3C validator