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  3489  reupick  3493  po2nr  4412  fvmptt  5747  fliftfund  5948  f1ocnv2d  6237  addclpi  7590  addnidpig  7599  mulnqprl  7831  mulnqpru  7832  ltsubrp  9969  ltaddrp  9970  pfxccat3  11364  divgcdcoprm0  12736  infpnlem1  12995  imasmnd2  13598  imasgrp2  13760  imasrng  14033  imasring  14141  innei  14957  tgcnp  15003  isxmetd  15141  2lgslem1a1  15888