Theorem imp32 255

Description: An importation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
imp3.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
imp32	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Proof of Theorem imp32

Step	Hyp	Ref	Expression
1		imp3.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	impd 252	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	imp 123	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem is referenced by:  imp42  351  impr  376  anasss  396  an13s  556  3expb  1182  reuss2  3356  reupick  3360  po2nr  4231  fvmptt  5512  fliftfund  5698  f1ocnv2d  5974  addclpi  7135  addnidpig  7144  mulnqprl  7376  mulnqpru  7377  ltsubrp  9478  ltaddrp  9479  divgcdcoprm0  11782  innei  12332  tgcnp  12378  isxmetd  12516