Theorem 3impd 1273

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 90	. . 3 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏))))
3	2	3imp 1249	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → (𝜑 → 𝜏))
4	3	com12 32	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))

Syntax hints:   → wi 4   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3imp2  1274  3impexp  1281  oprabid  6554  wfrlem12  7291  isinf  8036  axdc3lem4  9136  iccid  12050  difreicc  12134  relexpaddg  13590  issubg4  17385  reconn  22387  bcthlem2  22875  dvfsumrlim3  23545  ax5seg  25564  axcontlem4  25593  3v3e3cycl1  25966  4cycl4v4e  25988  4cycl4dv4e  25990  2spontn0vne  26208  eupai  26288  cvmlift3lem4  30352  frrlem11  30830  fscgr  31151  idinside  31155  brsegle  31179  seglecgr12im  31181  imp5q  31270  elicc3  31275  areacirclem1  32464  areacirclem2  32465  areacirclem4  32467  areacirc  32469  filbcmb  32499  fzmul  32501  islshpcv  33152  cvrat3  33540  4atexlem7  34173  relexpmulg  36815  gneispacess2  37258  iunconlem2  37987  fmtnoprmfac1  39810  fmtnoprmfac2  39812  fundmge2nop0  40142  usgr2wlkneq  40954