Theorem 3impd 1349

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

This theorem is referenced by:  3imp2  1350  3impexp  1359  po2ne  5540  oprabidw  7377  oprabid  7378  isinf  9149  infsupprpr  9390  axdc3lem4  10344  iccid  13290  difreicc  13384  fvf1tp  13693  relexpaddg  14960  issubg4  19058  rnglidlmcl  21154  reconn  24745  bcthlem2  25253  dvfsumrlim3  25968  ax5seg  28917  axcontlem4  28946  usgr2wlkneq  29735  frgrwopreg  30301  dfufd2lem  33512  cvmlift3lem4  35364  fscgr  36120  idinside  36124  brsegle  36148  seglecgr12im  36150  imp5q  36352  elicc3  36357  areacirclem1  37754  areacirclem2  37755  areacirclem4  37757  areacirc  37759  filbcmb  37786  fzmul  37787  islshpcv  39098  cvrat3  39487  4atexlem7  40120  relexpmulg  43749  gneispacess2  44185  iunconnlem2  44973  fmtnoprmfac1  47602  fmtnoprmfac2  47604  fpprwppr  47776  grimgrtri  47986  usgrgrtrirex  47987  grlimgrtri  48040  itsclc0xyqsol  48806