Theorem imp31 254

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 123	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
3	2	imp 123	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem is referenced by:  imp41  350  imp5d  356  impl  377  anassrs  397  an31s  559  con4biddc  842  3imp  1175  3expa  1181  bilukdc  1374  reusv3  4376  dfimafn  5463  funimass4  5465  funimass3  5529  isopolem  5716  smores2  6184  tfrlem9  6209  nnmordi  6405  mulcanpig  7136  elnnz  9057  nzadd  9099  irradd  9431  irrmul  9432  uzsubsubfz  9820  fzo1fzo0n0  9953  elfzonelfzo  10000  tgcl  12222