Theorem imp31 252

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  imp41  345  imp5d  351  impl  372  anassrs  392  an31s  537  con4biddc  792  3imp  1137  3expa  1143  bilukdc  1332  reusv3  4282  dfimafn  5353  funimass4  5355  funimass3  5415  isopolem  5601  smores2  6059  tfrlem9  6084  nnmordi  6273  mulcanpig  6892  elnnz  8758  nzadd  8800  irradd  9129  irrmul  9130  uzsubsubfz  9459  fzo1fzo0n0  9590  elfzonelfzo  9637