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  3444  reupick  3448  po2nr  4345  fvmptt  5656  fliftfund  5847  f1ocnv2d  6131  addclpi  7413  addnidpig  7422  mulnqprl  7654  mulnqpru  7655  ltsubrp  9784  ltaddrp  9785  divgcdcoprm0  12296  infpnlem1  12555  imasmnd2  13156  imasgrp2  13318  imasrng  13590  imasring  13698  innei  14507  tgcnp  14553  isxmetd  14691  2lgslem1a1  15435