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  352  impr  377  anasss  397  an13s  557  3expb  1183  reuss2  3361  reupick  3365  po2nr  4239  fvmptt  5520  fliftfund  5706  f1ocnv2d  5982  addclpi  7159  addnidpig  7168  mulnqprl  7400  mulnqpru  7401  ltsubrp  9507  ltaddrp  9508  divgcdcoprm0  11818  innei  12371  tgcnp  12417  isxmetd  12555