Theorem imp31 254

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 123	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
3	2	imp 123	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem is referenced by:  imp41  351  imp5d  357  impl  378  anassrs  398  an31s  560  con4biddc  843  3imp  1176  3expa  1182  bilukdc  1375  reusv3  4389  dfimafn  5478  funimass4  5480  funimass3  5544  isopolem  5731  smores2  6199  tfrlem9  6224  nnmordi  6420  mulcanpig  7167  elnnz  9088  nzadd  9130  irradd  9465  irrmul  9466  uzsubsubfz  9858  fzo1fzo0n0  9991  elfzonelfzo  10038  tgcl  12272