Theorem imp32 253

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 251	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	imp 122	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  imp42  346  impr  371  anasss  391  an13s  534  3expb  1144  reuss2  3279  reupick  3283  po2nr  4136  fvmptt  5394  fliftfund  5576  f1ocnv2d  5848  addclpi  6884  addnidpig  6893  mulnqprl  7125  mulnqpru  7126  ltsubrp  9166  ltaddrp  9167  divgcdcoprm0  11357