NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  exp31 GIF version

Theorem exp31 587
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 423 . 2 ((φ ψ) → (χθ))
32ex 423 1 (φ → (ψ → (χθ)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   wa 358
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 177  df-an 360
This theorem is referenced by:  exp41  593  exp42  594  expl  601  exbiri  605  anasss  628  an31s  781  3impa  1146  exp516  1171  ax11indalem  2197  ax11inda2ALT  2198  nndisjeq  4429  dffo3  5422  fconstfv  5456
  Copyright terms: Public domain W3C validator