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  4507  dfimafn  5627  funimass4  5629  funimass3  5696  isopolem  5891  smores2  6380  tfrlem9  6405  nnmordi  6602  mulcanpig  7448  elnnz  9382  nzadd  9425  irradd  9767  irrmul  9768  uzsubsubfz  10169  fzo1fzo0n0  10307  elincfzoext  10322  elfzonelfzo  10359  swrdwrdsymbg  11117  infpnlem1  12682  tgcl  14536