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  4399  fvmptt  5725  fliftfund  5920  f1ocnv2d  6208  addclpi  7510  addnidpig  7519  mulnqprl  7751  mulnqpru  7752  ltsubrp  9882  ltaddrp  9883  pfxccat3  11261  divgcdcoprm0  12618  infpnlem1  12877  imasmnd2  13480  imasgrp2  13642  imasrng  13914  imasring  14022  innei  14831  tgcnp  14877  isxmetd  15015  2lgslem1a1  15759