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  1230  reuss2  3487  reupick  3491  po2nr  4406  fvmptt  5738  fliftfund  5938  f1ocnv2d  6227  addclpi  7547  addnidpig  7556  mulnqprl  7788  mulnqpru  7789  ltsubrp  9925  ltaddrp  9926  pfxccat3  11319  divgcdcoprm0  12678  infpnlem1  12937  imasmnd2  13540  imasgrp2  13702  imasrng  13975  imasring  14083  innei  14893  tgcnp  14939  isxmetd  15077  2lgslem1a1  15821