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  862  3imp  1217  3expa  1227  bilukdc  1438  reusv3  4550  dfimafn  5681  funimass4  5683  funimass3  5750  isopolem  5945  smores2  6438  tfrlem9  6463  nnmordi  6660  mulcanpig  7518  elnnz  9452  nzadd  9495  irradd  9837  irrmul  9838  uzsubsubfz  10239  fzo1fzo0n0  10379  elincfzoext  10394  elfzonelfzo  10431  swrdwrdsymbg  11191  wrd2ind  11250  infpnlem1  12877  tgcl  14732