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 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is used by:  imp41  353  imp5d  359  impl  380  anassrs  404  an31s  576  con4biddc  869  3imp  1224  3expa  1234  bilukdc  1445  reusv3  4606  dfimafn  5751  funimass4  5753  funimass3  5825  dfimafnf  5955  isopolem  6028  suppfnss  6497  smores2  6565  tfrlem9  6590  nnmordi  6789  mulcanpig  7702  elnnz  9654  nzadd  9697  irradd  10046  irrmul  10047  uzsubsubfz  10452  fzo1fzo0n0  10595  elincfzoext  10611  elfzonelfzo  10648  swrdwrdsymbg  11436  wrd2ind  11495  infpnlem1  13138  tgcl  15165  uspgr2wlkeqi  16608  clwwlkext2edg  16663  clwwlknonex2lem2  16679