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

Theorem exp4b 364
 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 363 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
 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  369  reuss2  3356  nndi  6382  mulnqprl  7388  mulnqpru  7389  distrlem5prl  7406  distrlem5pru  7407  recexprlemss1l  7455  recexprlemss1u  7456  lemul12a  8632  nnmulcl  8753  elfz0fzfz0  9915  fzo1fzo0n0  9972  fzofzim  9977  elfzodifsumelfzo  9990  le2sq2  10380  oddprmgt2  11825
 Copyright terms: Public domain W3C validator