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  5545  oprabidw  7385  oprabid  7386  isinf  9158  infsupprpr  9399  axdc3lem4  10353  iccid  13294  difreicc  13388  fvf1tp  13697  relexpaddg  14964  issubg4  19062  rnglidlmcl  21157  reconn  24747  bcthlem2  25255  dvfsumrlim3  25970  ax5seg  28920  axcontlem4  28949  usgr2wlkneq  29738  frgrwopreg  30307  dfufd2lem  33523  cvmlift3lem4  35389  fscgr  36147  idinside  36151  brsegle  36175  seglecgr12im  36177  imp5q  36379  elicc3  36384  areacirclem1  37771  areacirclem2  37772  areacirclem4  37774  areacirc  37776  filbcmb  37803  fzmul  37804  islshpcv  39175  cvrat3  39564  4atexlem7  40197  relexpmulg  43830  gneispacess2  44266  iunconnlem2  45054  fmtnoprmfac1  47692  fmtnoprmfac2  47694  fpprwppr  47866  grimgrtri  48076  usgrgrtrirex  48077  grlimgrtri  48130  itsclc0xyqsol  48896