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  403  an13s  573  3expb  1235  reuss2  3513  reupick  3517  po2nr  4449  fvmptt  5791  fliftfund  5993  f1ocnv2d  6284  f1o3d  6288  addclpi  7684  addnidpig  7693  mulnqprl  7925  mulnqpru  7926  ltsubrp  10070  ltaddrp  10071  pfxccat3  11484  divgcdcoprm0  12857  infpnlem1  13116  imasmnd2  13736  imasgrp2  13890  imasrng  14230  imasring  14342  innei  15187  tgcnp  15233  isxmetd  15371  2lgslem1a1  16119