Theorem imp32 257

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

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  imp42  354  impr  379  anasss  399  an13s  569  3expb  1231  reuss2  3501  reupick  3505  po2nr  4430  fvmptt  5769  fliftfund  5970  f1ocnv2d  6259  addclpi  7642  addnidpig  7651  mulnqprl  7883  mulnqpru  7884  ltsubrp  10023  ltaddrp  10024  pfxccat3  11426  divgcdcoprm0  12798  infpnlem1  13057  imasmnd2  13665  imasgrp2  13827  imasrng  14100  imasring  14208  innei  15028  tgcnp  15074  isxmetd  15212  2lgslem1a1  15959