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

Theorem 3expa 1151
 Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3exp.1 ((φ ψ χ) → θ)
Assertion
Ref Expression
3expa (((φ ψ) χ) → θ)

Proof of Theorem 3expa
StepHypRef Expression
1 3exp.1 . . 3 ((φ ψ χ) → θ)
213exp 1150 . 2 (φ → (ψ → (χθ)))
32imp31 421 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:  3anidm23  1241  mp3an2  1265  mpd3an3  1278  rgen3  2711  moi2  3017  sbc3ie  3115  preq12bg  4128  eladdci  4399  nnsucelr  4428  nndisjeq  4429  leltfintr  4458  nnpw1ex  4484  tfinpw1  4494  tfinltfinlem1  4500  tfinltfin  4501  sfin112  4529  sfindbl  4530  sfinltfin  4535  vfinncvntnn  4548  nenpw1pwlem2  6085  ncspw1eu  6159  letc  6231  ce2le  6233
 Copyright terms: Public domain W3C validator