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  1185  bilukdc  1378  reusv3  4419  dfimafn  5516  funimass4  5518  funimass3  5582  isopolem  5769  smores2  6238  tfrlem9  6263  nnmordi  6460  mulcanpig  7249  elnnz  9171  nzadd  9213  irradd  9548  irrmul  9549  uzsubsubfz  9942  fzo1fzo0n0  10075  elfzonelfzo  10122  tgcl  12435