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

Theorem exp4b 349
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)
Hypothesis
Ref Expression
exp4b.1 ((φ ψ) → ((χ θ) → τ))
Assertion
Ref Expression
exp4b (φ → (ψ → (χ → (θτ))))

Proof of Theorem exp4b
StepHypRef Expression
1 exp4b.1 . . 3 ((φ ψ) → ((χ θ) → τ))
21ex 108 . 2 (φ → (ψ → ((χ θ) → τ)))
32exp4a 348 1 (φ → (ψ → (χ → (θτ))))
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 depends on definitions:  df-bi 110
This theorem is referenced by:  exp43  354  reuss2  3214  nndi  6008  mulnqprl  6556  mulnqpru  6557  distrlem5prl  6574  distrlem5pru  6575  recexprlemss1l  6623  recexprlemss1u  6624  lemul12a  7701  nnmulcl  7808  elfz0fzfz0  8845  fzo1fzo0n0  8901  fzofzim  8906  elfzodifsumelfzo  8919  le2sq2  9075
  Copyright terms: Public domain W3C validator