Theorem 3impd 1367

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

Syntax hints:   → wi 4   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  3imp2  1368  3impexp  1377  po2ne  5587  oprabidw  7443  oprabid  7444  isinf  9226  infsupprpr  9467  axdc3lem4  10438  iccid  13418  difreicc  13512  fvf1tp  13824  relexpaddg  15092  issubg4  19213  rnglidlmcl  21322  reconn  24967  bcthlem2  25465  dvfsumrlim3  26173  ax5seg  29269  axcontlem4  29298  usgr2wlkneq  30086  frgrwopreg  30655  dfufd2lem  33820  cvmlift3lem4  35795  fscgr  36553  idinside  36557  brsegle  36581  seglecgr12im  36583  imp5q  36805  elicc3  36809  areacirclem1  38340  areacirclem2  38341  areacirclem4  38343  areacirc  38345  filbcmb  38372  fzmul  38373  islshpcv  39808  cvrat3  40197  4atexlem7  40830  relexpmulg  44419  gneispacess2  44855  iunconnlem2  45626  fmtnoprmfac1  48300  fmtnoprmfac2  48302  fpprwppr  48487  grimgrtri  48697  usgrgrtrirex  48698  grlimgrtri  48751  itsclc0xyqsol  49531