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

Theorem exp4b 353
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 112 . 2 (𝜑 → (𝜓 → ((𝜒𝜃) → 𝜏)))
32exp4a 352 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  exp43  358  reuss2  3245  nndi  6096  mulnqprl  6724  mulnqpru  6725  distrlem5prl  6742  distrlem5pru  6743  recexprlemss1l  6791  recexprlemss1u  6792  lemul12a  7903  nnmulcl  8011  elfz0fzfz0  9085  fzo1fzo0n0  9141  fzofzim  9146  elfzodifsumelfzo  9159  le2sq2  9495
  Copyright terms: Public domain W3C validator