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  4551  dfimafn  5684  funimass4  5686  funimass3  5753  isopolem  5952  smores2  6446  tfrlem9  6471  nnmordi  6670  mulcanpig  7533  elnnz  9467  nzadd  9510  irradd  9853  irrmul  9854  uzsubsubfz  10255  fzo1fzo0n0  10395  elincfzoext  10411  elfzonelfzo  10448  swrdwrdsymbg  11211  wrd2ind  11270  infpnlem1  12897  tgcl  14753  uspgr2wlkeqi  16108