Theorem imp31 256

Description: An importation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
imp3.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
imp31	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem imp31

Step	Hyp	Ref	Expression
1		imp3.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	imp 124	. 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:  imp41  353  imp5d  359  impl  380  anassrs  400  an31s  570  con4biddc  859  3imp  1196  3expa  1206  bilukdc  1416  reusv3  4520  dfimafn  5645  funimass4  5647  funimass3  5714  isopolem  5909  smores2  6398  tfrlem9  6423  nnmordi  6620  mulcanpig  7478  elnnz  9412  nzadd  9455  irradd  9797  irrmul  9798  uzsubsubfz  10199  fzo1fzo0n0  10339  elincfzoext  10354  elfzonelfzo  10391  swrdwrdsymbg  11150  wrd2ind  11209  infpnlem1  12767  tgcl  14621