Theorem 3impb 610

Description: Importation from double to triple conjunction.

Hypothesis

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

Assertion

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

Proof of Theorem 3impb

Step	Hyp	Ref	Expression
1		3impb.1	. . 3 ⊢ ((φ ∧ (ψ ∧ χ)) → θ)
2	1	exp32 294	. 2 ⊢ (φ → (ψ → (χ → θ)))
3	2	3imp 608	1 ⊢ ((φ ∧ ψ ∧ χ) → θ)

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

This theorem is referenced by:  syl3an1 619  3impdi 630  nndi 3180  ecopoprtrn 3247  ecoprass 3256  ecoprdi 3257  addasspi 3817  mulasspi 3819  distrpi 3820  ltapq 3870  ltmpq 3871  genpass 3906  distrpr 3926  ltapr 3945  subsubt 4203  le2tri3 4311  ltaddsubt 4357  his5 5050  his7 5051  atcvat2t 5773

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