Theorem 3impd 1350

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  1351  3impexp  1360  po2ne  5548  oprabidw  7391  oprabid  7392  isinf  9168  infsupprpr  9412  axdc3lem4  10366  iccid  13334  difreicc  13428  fvf1tp  13739  relexpaddg  15006  issubg4  19112  rnglidlmcl  21206  reconn  24804  bcthlem2  25302  dvfsumrlim3  26010  ax5seg  29021  axcontlem4  29050  usgr2wlkneq  29839  frgrwopreg  30408  dfufd2lem  33624  cvmlift3lem4  35520  fscgr  36278  idinside  36282  brsegle  36306  seglecgr12im  36308  imp5q  36510  elicc3  36515  areacirclem1  38043  areacirclem2  38044  areacirclem4  38046  areacirc  38048  filbcmb  38075  fzmul  38076  islshpcv  39513  cvrat3  39902  4atexlem7  40535  relexpmulg  44155  gneispacess2  44591  iunconnlem2  45379  fmtnoprmfac1  48040  fmtnoprmfac2  48042  fpprwppr  48227  grimgrtri  48437  usgrgrtrirex  48438  grlimgrtri  48491  itsclc0xyqsol  49256