Theorem 3impd 1442

Description: Importation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)

Hypothesis

Ref	Expression
3imp1.1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Assertion

Ref	Expression
3impd	⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))

Proof of Theorem 3impd

Step	Hyp	Ref	Expression
1		3imp1.1	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2	1	com4l 92	. . 3 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏))))
3	2	3imp 1102	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → (𝜑 → 𝜏))
4	3	com12 32	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))

Syntax hints:   → wi 4   ∧ w3a 1072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 385  df-3an 1074

This theorem is referenced by:  3imp2  1443  3impexp  1452  oprabid  6841  wfrlem12  7596  isinf  8340  axdc3lem4  9487  iccid  12433  difreicc  12517  relexpaddg  14012  issubg4  17834  reconn  22852  bcthlem2  23342  dvfsumrlim3  24015  ax5seg  26038  axcontlem4  26067  usgr2wlkneq  26883  frgrwopreg  27498  cvmlift3lem4  31632  fscgr  32514  idinside  32518  brsegle  32542  seglecgr12im  32544  imp5q  32633  elicc3  32638  areacirclem1  33831  areacirclem2  33832  areacirclem4  33834  areacirc  33836  filbcmb  33866  fzmul  33868  islshpcv  34861  cvrat3  35249  4atexlem7  35882  relexpmulg  38522  gneispacess2  38964  iunconnlem2  39688  fmtnoprmfac1  42005  fmtnoprmfac2  42007