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  572  con4biddc  865  3imp  1220  3expa  1230  bilukdc  1441  reusv3  4563  dfimafn  5703  funimass4  5705  funimass3  5772  isopolem  5973  suppfnss  6435  smores2  6503  tfrlem9  6528  nnmordi  6727  mulcanpig  7598  elnnz  9533  nzadd  9576  irradd  9924  irrmul  9925  uzsubsubfz  10327  fzo1fzo0n0  10468  elincfzoext  10484  elfzonelfzo  10521  swrdwrdsymbg  11294  wrd2ind  11353  infpnlem1  12995  tgcl  14858  uspgr2wlkeqi  16291  clwwlkext2edg  16346  clwwlknonex2lem2  16362