Theorem 3imp 608

Description: Importation inference.

Hypothesis

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

Assertion

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

Proof of Theorem 3imp

Step	Hyp	Ref	Expression
1		df-3an 583	. 2 ⊢ ((φ ∧ ψ ∧ χ) ↔ ((φ ∧ ψ) ∧ χ))
2		3imp.1	. . 3 ⊢ (φ → (ψ → (χ → θ)))
3	2	imp31 280	. 2 ⊢ (((φ ∧ ψ) ∧ χ) → θ)
4	1, 3	sylbi 174	1 ⊢ ((φ ∧ ψ ∧ χ) → θ)

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

This theorem is referenced by:  3impa 609  3impb 610  3com12 614  3com23 616  syl3an2 620  syl3an3 621  3jao 632  3gencl 1367  vtocl3ga 1389  dedth3h 1788  oawordri 3152  oaass 3163  nndi 3180  nnmass 3181  nnmordi 3188  3ecoptocl 3241  eceqopreq 3249  addsubt 4151  divasst 4239  div23t 4240  expaddt 4698  spansncol 5473

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