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

Theorem 3impia 1148
 Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
Hypothesis
Ref Expression
3impia.1 ((φ ψ) → (χθ))
Assertion
Ref Expression
3impia ((φ ψ χ) → θ)

Proof of Theorem 3impia
StepHypRef Expression
1 3impia.1 . . 3 ((φ ψ) → (χθ))
21ex 423 . 2 (φ → (ψ → (χθ)))
323imp 1145 1 ((φ ψ χ) → θ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 358   ∧ w3a 934 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936 This theorem is referenced by:  mopick2  2271  3gencl  2889  mob2  3016  moi  3019  reupick3  3540  disjne  3596  tfindi  4496  sfin112  4529  sfinltfin  4535  vfintle  4546  fvun1  5379  ovmpt4g  5710  ov2gf  5711  letc  6231  nclenn  6249  nchoicelem9  6297  nchoicelem17  6305  frecxp  6314
 Copyright terms: Public domain W3C validator