ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  exp31 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  6478  genpcdl  6502  genpcuu  6503  recexap  7416  zaddcllemneg  8060  zdiv  8104  uzaddcl  8305  fz0fzelfz0  8754  fz0fzdiffz0  8757  elfzmlbp  8760  difelfzle  8762  fzo1fzo0n0  8809  ssfzo12bi  8851  expivallem  8910  expcllem  8920  expap0  8939  mulexp  8948  cjexp  9121
  Copyright terms: Public domain W3C validator