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

Theorem exp4b 360
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 114 . 2 (𝜑 → (𝜓 → ((𝜒𝜃) → 𝜏)))
32exp4a 359 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  exp43  365  reuss2  3282  nndi  6263  mulnqprl  7190  mulnqpru  7191  distrlem5prl  7208  distrlem5pru  7209  recexprlemss1l  7257  recexprlemss1u  7258  lemul12a  8386  nnmulcl  8506  elfz0fzfz0  9600  fzo1fzo0n0  9657  fzofzim  9662  elfzodifsumelfzo  9675  le2sq2  10093  oddprmgt2  11456
  Copyright terms: Public domain W3C validator