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  858  3imp  1195  3expa  1205  bilukdc  1415  reusv3  4506  dfimafn  5626  funimass4  5628  funimass3  5695  isopolem  5890  smores2  6379  tfrlem9  6404  nnmordi  6601  mulcanpig  7447  elnnz  9381  nzadd  9424  irradd  9766  irrmul  9767  uzsubsubfz  10168  fzo1fzo0n0  10305  elincfzoext  10320  elfzonelfzo  10357  infpnlem1  12653  tgcl  14507