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  404  an31s  576  con4biddc  869  3imp  1224  3expa  1234  bilukdc  1445  reusv3  4601  dfimafn  5745  funimass4  5747  funimass3  5816  dfimafnf  5945  isopolem  6018  suppfnss  6487  smores2  6555  tfrlem9  6580  nnmordi  6779  mulcanpig  7692  elnnz  9633  nzadd  9676  irradd  10025  irrmul  10026  uzsubsubfz  10430  fzo1fzo0n0  10573  elincfzoext  10589  elfzonelfzo  10626  swrdwrdsymbg  11414  wrd2ind  11473  infpnlem1  13116  tgcl  15088  uspgr2wlkeqi  16522  clwwlkext2edg  16577  clwwlknonex2lem2  16593