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  4581  dfimafn  5725  funimass4  5727  funimass3  5794  isopolem  5995  suppfnss  6457  smores2  6525  tfrlem9  6550  nnmordi  6749  mulcanpig  7650  elnnz  9587  nzadd  9630  irradd  9978  irrmul  9979  uzsubsubfz  10381  fzo1fzo0n0  10522  elincfzoext  10538  elfzonelfzo  10575  swrdwrdsymbg  11356  wrd2ind  11415  infpnlem1  13057  tgcl  14929  uspgr2wlkeqi  16362  clwwlkext2edg  16417  clwwlknonex2lem2  16433