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  3217  nndi  6065  mulnqprl  6666  mulnqpru  6667  distrlem5prl  6684  distrlem5pru  6685  recexprlemss1l  6733  recexprlemss1u  6734  lemul12a  7828  nnmulcl  7935  elfz0fzfz0  8983  fzo1fzo0n0  9039  fzofzim  9044  elfzodifsumelfzo  9057  le2sq2  9329
 Copyright terms: Public domain W3C validator