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  1228  reuss2  3484  reupick  3488  po2nr  4400  fvmptt  5728  fliftfund  5927  f1ocnv2d  6216  addclpi  7525  addnidpig  7534  mulnqprl  7766  mulnqpru  7767  ltsubrp  9898  ltaddrp  9899  pfxccat3  11281  divgcdcoprm0  12638  infpnlem1  12897  imasmnd2  13500  imasgrp2  13662  imasrng  13934  imasring  14042  innei  14852  tgcnp  14898  isxmetd  15036  2lgslem1a1  15780