Theorem 3expa 1088

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

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((φ ∧ ψ ∧ χ) → θ)
2	1	3exp 1087	. 2 ⊢ (φ → (ψ → (χ → θ)))
3	2	imp31 243	1 ⊢ (((φ ∧ ψ) ∧ χ) → θ)

Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 871

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 873

This theorem is referenced by:  3anidm23  1178  mp3an2  1203  mpd3an3  1216  rgen3  2380  moi2  2695  sbc3ie  2804  preq12bg  3514  issod  4026  reuhypd  4149  funimass4  5145  fvtp1g  5290  f1imass  5334  fcof1o  5350  f1ofveu  5420  f1ocnvfv3  5421  acexmid  5431  2ndrn  5728  rdgon  5889  frecrdg  5904  ltapig  6192  ltanqi  6255  ltmnqi  6256  lt2addnq  6257  ltbtwnnqq  6266  prarloclemcalc  6350  genpassl  6373  genpassu  6374  prmuloc  6404  ltexprlemm  6431  ltexprlemfl  6440  ltexprlemfu  6442  ltaprg  6449  mul4  6732  add4  6759  cnegexlem2  6774  cnegexlem3  6775  2addsub  6812  addsubeq4  6813  muladd  6967  ltleadd  7026