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

Theorem 3expia 1153
Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
Hypothesis
Ref Expression
3exp.1 ((φ ψ χ) → θ)
Assertion
Ref Expression
3expia ((φ ψ) → (χθ))

Proof of Theorem 3expia
StepHypRef Expression
1 3exp.1 . . 3 ((φ ψ χ) → θ)
213exp 1150 . 2 (φ → (ψ → (χθ)))
32imp 418 1 ((φ ψ) → (χθ))
Colors of variables: wff setvar class
Syntax hints:  wi 4   wa 358   w3a 934
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  df-3an 936
This theorem is referenced by:  mp3an3  1266  3gencl  2889  moi  3019  ltfintri  4466  tfindi  4496  nnadjoin  4520  nnpweq  4523  sfintfin  4532  tfinnn  4534  sfinltfin  4535  vfintle  4546  suc11nnc  4558  phi11lem1  4595  3optocl  4840  ndmovord  5620  ov2gf  5711  antird  5928  iserd  5942  mapvalg  6009  enprmaplem5  6080  enprmaplem6  6081  nclenc  6222  lenc  6223  nclenn  6249  nchoicelem17  6305  nchoicelem19  6307  fnfreclem3  6319
  Copyright terms: Public domain W3C validator