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  4555  dfimafn  5690  funimass4  5692  funimass3  5759  isopolem  5958  smores2  6455  tfrlem9  6480  nnmordi  6679  mulcanpig  7545  elnnz  9479  nzadd  9522  irradd  9870  irrmul  9871  uzsubsubfz  10272  fzo1fzo0n0  10412  elincfzoext  10428  elfzonelfzo  10465  swrdwrdsymbg  11235  wrd2ind  11294  infpnlem1  12922  tgcl  14778  uspgr2wlkeqi  16164  clwwlkext2edg  16217  clwwlknonex2lem2  16233