Theorem imp31 243

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

Syntax hints:   → wi 4   ∧ wa 97

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

This theorem is referenced by:  imp41  335  imp5d  341  impl  362  anassrs  380  an31s  504  con4biddc  754  3imp  1098  3expa  1104  bilukdc  1287  reusv3  4192  dfimafn  5222  funimass4  5224  funimass3  5283  isopolem  5461  smores2  5909  tfrlem9  5935  nnmordi  6089  mulcanpig  6433  elnnz  8255  irradd  8580  irrmul  8581  uzsubsubfz  8911  fzo1fzo0n0  9039  elfzonelfzo  9086