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

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

Proof of Theorem 3impb
StepHypRef Expression
1 3impb.1 . . 3 ((φ (ψ χ)) → θ)
21exp32 588 . 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-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:  3adant1l  1174  3adant1r  1175  3impdi  1237  vtocl3gf  2917  rspc2ev  2963  reuss  3536  pw1equn  4331  pw1eqadj  4332  preaddccan2  4455  resdif  5306  fnopovb  5557  fovrn  5604  fnovrn  5607  mucass  6135  addccan2nc  6265  nchoicelem3  6291
 Copyright terms: Public domain W3C validator