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 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is used by:  imp42  354  impr  379  anasss  403  an13s  573  3expb  1235  reuss2  3513  reupick  3517  po2nr  4456  fvmptt  5800  fliftfund  6006  f1ocnv2d  6297  f1o3d  6301  addclpi  7700  addnidpig  7709  mulnqprl  7941  mulnqpru  7942  ltsubrp  10108  ltaddrp  10109  pfxccat3  11528  divgcdcoprm0  12904  infpnlem1  13167  imasmnd2  13818  imasgrp2  13972  imasrng  14362  imasring  14478  innei  15389  tgcnp  15435  isxmetd  15573  2lgslem1a1  16410