Theorem 3expa 612

Description: Exportation from triple to double conjunction.

Hypothesis

Ref	Expression
3exp.1	⊢ ((φ ∧ ψ ∧ χ) → θ)

Assertion

Ref	Expression
3expa	⊢ (((φ ∧ ψ) ∧ χ) → θ)

Proof of Theorem 3expa

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

Syntax hints:   → wi 2   ∧ wa 196   ∧ w3a 581

This theorem is referenced by:  mp3an2 640  mp3an3 641  3optocl 2471  oalimcl 3162  cdavalt 3716  ltapi 3824  add4t 4127  mul4t 4177  zbtwnre 4619  qbtwnre 4650  seqrn2 4674  hvadd4t 5013  ocsh 5164  occllem6 5185  projlem25 5217  projlem26 5218  spansncol 5473  atcvatlem 5770  mdsymlem3 5778  mdsymlem5 5780  sumdmdi 5785  sumdmdlem 5786

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198  df-3an 583

metamath.org