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  857  3imp  1193  3expa  1203  bilukdc  1396  reusv3  4461  dfimafn  5565  funimass4  5567  funimass3  5633  isopolem  5823  smores2  6295  tfrlem9  6320  nnmordi  6517  mulcanpig  7334  elnnz  9263  nzadd  9305  irradd  9646  irrmul  9647  uzsubsubfz  10047  fzo1fzo0n0  10183  elfzonelfzo  10230  infpnlem1  12357  tgcl  13567