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

Theorem exp31 346
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp31.1 (((φ ψ) χ) → θ)
Assertion
Ref Expression
exp31 (φ → (ψ → (χθ)))

Proof of Theorem exp31
StepHypRef Expression
1 exp31.1 . . 3 (((φ ψ) χ) → θ)
21ex 108 . 2 ((φ ψ) → (χθ))
32ex 108 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-ia3 101
This theorem is referenced by:  exp41  352  exp42  353  expl  360  exbiri  364  anasss  379  an31s  504  con4biddc  753  3impa  1098  exp516  1123  r19.29af2  2446  mpteqb  5204  dffo3  5257  fconstfvm  5322  fliftfun  5379  tfrlem1  5864  tfrlem9  5876  nnsucsssuc  6010  nnaordex  6036  prarloclemup  6477  genpcdl  6501  genpcuu  6502  recexap  7396  zaddcllemneg  8040  zdiv  8084  uzaddcl  8285  fz0fzelfz0  8734  fz0fzdiffz0  8737  elfzmlbp  8740  difelfzle  8742  fzo1fzo0n0  8789  ssfzo12bi  8831  expivallem  8890  expcllem  8900  expap0  8919  mulexp  8928  cjexp  9101
  Copyright terms: Public domain W3C validator