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  5562  oprabidw  7418  oprabid  7419  isinf  9207  isinfOLD  9208  infsupprpr  9457  axdc3lem4  10406  iccid  13351  difreicc  13445  fvf1tp  13751  relexpaddg  15019  issubg4  19077  rnglidlmcl  21126  reconn  24717  bcthlem2  25225  dvfsumrlim3  25940  ax5seg  28865  axcontlem4  28894  usgr2wlkneq  29686  frgrwopreg  30252  dfufd2lem  33520  cvmlift3lem4  35309  fscgr  36068  idinside  36072  brsegle  36096  seglecgr12im  36098  imp5q  36300  elicc3  36305  areacirclem1  37702  areacirclem2  37703  areacirclem4  37705  areacirc  37707  filbcmb  37734  fzmul  37735  islshpcv  39046  cvrat3  39436  4atexlem7  40069  relexpmulg  43699  gneispacess2  44135  iunconnlem2  44924  fmtnoprmfac1  47566  fmtnoprmfac2  47568  fpprwppr  47740  grimgrtri  47948  usgrgrtrirex  47949  grlimgrtri  47995  itsclc0xyqsol  48757