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  572  con4biddc  864  3imp  1219  3expa  1229  bilukdc  1440  reusv3  4557  dfimafn  5694  funimass4  5696  funimass3  5763  isopolem  5963  smores2  6460  tfrlem9  6485  nnmordi  6684  mulcanpig  7555  elnnz  9489  nzadd  9532  irradd  9880  irrmul  9881  uzsubsubfz  10282  fzo1fzo0n0  10423  elincfzoext  10439  elfzonelfzo  10476  swrdwrdsymbg  11249  wrd2ind  11308  infpnlem1  12937  tgcl  14794  uspgr2wlkeqi  16224  clwwlkext2edg  16279  clwwlknonex2lem2  16295