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  6576  wfrlem12  7313  isinf  8058  axdc3lem4  9158  iccid  12091  difreicc  12175  fundmge2nop0  13129  relexpaddg  13641  issubg4  17436  reconn  22439  bcthlem2  22930  dvfsumrlim3  23600  ax5seg  25618  axcontlem4  25647  3v3e3cycl1  26172  4cycl4v4e  26194  4cycl4dv4e  26196  2spontn0vne  26414  eupai  26494  cvmlift3lem4  30558  frrlem11  31036  fscgr  31357  idinside  31361  brsegle  31385  seglecgr12im  31387  imp5q  31476  elicc3  31481  areacirclem1  32670  areacirclem2  32671  areacirclem4  32673  areacirc  32675  filbcmb  32705  fzmul  32707  islshpcv  33358  cvrat3  33746  4atexlem7  34379  relexpmulg  37021  gneispacess2  37464  iunconlem2  38193  fmtnoprmfac1  40015  fmtnoprmfac2  40017  usgr2wlkneq  40962