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

Theorem exp4b 367
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 115 . 2 (𝜑 → (𝜓 → ((𝜒𝜃) → 𝜏)))
32exp4a 366 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
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  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  exp43  372  reuss2  3430  nndi  6511  mulnqprl  7597  mulnqpru  7598  distrlem5prl  7615  distrlem5pru  7616  recexprlemss1l  7664  recexprlemss1u  7665  lemul12a  8849  nnmulcl  8970  elfz0fzfz0  10156  fzo1fzo0n0  10213  fzofzim  10218  elfzodifsumelfzo  10231  le2sq2  10627  oddprmgt2  12166  infpnlem1  12391  lmodvsdi  13627
  Copyright terms: Public domain W3C validator