Theorem 3impd 1348

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3imp2  1349  3impexp  1358  po2ne  5624  oprabidw  7479  oprabid  7480  wfrlem12OLD  8376  isinf  9323  isinfOLD  9324  infsupprpr  9573  axdc3lem4  10522  iccid  13452  difreicc  13544  fvf1tp  13840  relexpaddg  15102  issubg4  19185  rnglidlmcl  21249  reconn  24869  bcthlem2  25378  dvfsumrlim3  26094  ax5seg  28971  axcontlem4  29000  usgr2wlkneq  29792  frgrwopreg  30355  dfufd2lem  33542  cvmlift3lem4  35290  fscgr  36044  idinside  36048  brsegle  36072  seglecgr12im  36074  imp5q  36278  elicc3  36283  areacirclem1  37668  areacirclem2  37669  areacirclem4  37671  areacirc  37673  filbcmb  37700  fzmul  37701  islshpcv  39009  cvrat3  39399  4atexlem7  40032  relexpmulg  43672  gneispacess2  44108  iunconnlem2  44906  fmtnoprmfac1  47439  fmtnoprmfac2  47441  fpprwppr  47613  grimgrtri  47798  usgrgrtrirex  47799  grlimgrtri  47820  itsclc0xyqsol  48502