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  3440  reupick  3444  po2nr  4341  fvmptt  5650  fliftfund  5841  f1ocnv2d  6124  addclpi  7389  addnidpig  7398  mulnqprl  7630  mulnqpru  7631  ltsubrp  9759  ltaddrp  9760  divgcdcoprm0  12242  infpnlem1  12500  imasgrp2  13183  imasrng  13455  imasring  13563  innei  14342  tgcnp  14388  isxmetd  14526  2lgslem1a1  15243