Theorem 3impd 1347

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3imp2  1348  3impexp  1357  po2ne  5519  oprabidw  7306  oprabid  7307  wfrlem12OLD  8151  isinf  9036  infsupprpr  9263  axdc3lem4  10209  iccid  13124  difreicc  13216  relexpaddg  14764  issubg4  18774  reconn  23991  bcthlem2  24489  dvfsumrlim3  25197  ax5seg  27306  axcontlem4  27335  usgr2wlkneq  28124  frgrwopreg  28687  cvmlift3lem4  33284  fscgr  34382  idinside  34386  brsegle  34410  seglecgr12im  34412  imp5q  34501  elicc3  34506  areacirclem1  35865  areacirclem2  35866  areacirclem4  35868  areacirc  35870  filbcmb  35898  fzmul  35899  islshpcv  37067  cvrat3  37456  4atexlem7  38089  relexpmulg  41318  gneispacess2  41756  iunconnlem2  42555  fmtnoprmfac1  45017  fmtnoprmfac2  45019  fpprwppr  45191  itsclc0xyqsol  46114