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

Theorem exp4b 365
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)
Hypothesis
Ref Expression
exp4b.1  |-  ( (
ph  /\  ps )  ->  ( ( ch  /\  th )  ->  ta )
)
Assertion
Ref Expression
exp4b  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )

Proof of Theorem exp4b
StepHypRef Expression
1 exp4b.1 . . 3  |-  ( (
ph  /\  ps )  ->  ( ( ch  /\  th )  ->  ta )
)
21ex 114 . 2  |-  ( ph  ->  ( ps  ->  (
( ch  /\  th )  ->  ta ) ) )
32exp4a 364 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  exp43  370  reuss2  3387  nndi  6433  mulnqprl  7488  mulnqpru  7489  distrlem5prl  7506  distrlem5pru  7507  recexprlemss1l  7555  recexprlemss1u  7556  lemul12a  8733  nnmulcl  8854  elfz0fzfz0  10025  fzo1fzo0n0  10082  fzofzim  10087  elfzodifsumelfzo  10100  le2sq2  10494  oddprmgt2  12011
  Copyright terms: Public domain W3C validator