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  864  3imp  1219  3expa  1229  bilukdc  1440  reusv3  4557  dfimafn  5694  funimass4  5696  funimass3  5763  isopolem  5962  smores2  6459  tfrlem9  6484  nnmordi  6683  mulcanpig  7554  elnnz  9488  nzadd  9531  irradd  9879  irrmul  9880  uzsubsubfz  10281  fzo1fzo0n0  10421  elincfzoext  10437  elfzonelfzo  10474  swrdwrdsymbg  11244  wrd2ind  11303  infpnlem1  12931  tgcl  14787  uspgr2wlkeqi  16217  clwwlkext2edg  16272  clwwlknonex2lem2  16288