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  567  3expb  1206  reuss2  3452  reupick  3456  po2nr  4355  fvmptt  5670  fliftfund  5865  f1ocnv2d  6149  addclpi  7439  addnidpig  7448  mulnqprl  7680  mulnqpru  7681  ltsubrp  9811  ltaddrp  9812  divgcdcoprm0  12394  infpnlem1  12653  imasmnd2  13255  imasgrp2  13417  imasrng  13689  imasring  13797  innei  14606  tgcnp  14652  isxmetd  14790  2lgslem1a1  15534