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  5582  oprabidw  7441  oprabid  7442  wfrlem12OLD  8339  isinf  9273  isinfOLD  9274  infsupprpr  9523  axdc3lem4  10472  iccid  13412  difreicc  13506  fvf1tp  13811  relexpaddg  15077  issubg4  19133  rnglidlmcl  21182  reconn  24773  bcthlem2  25282  dvfsumrlim3  25997  ax5seg  28922  axcontlem4  28951  usgr2wlkneq  29743  frgrwopreg  30309  dfufd2lem  33569  cvmlift3lem4  35349  fscgr  36103  idinside  36107  brsegle  36131  seglecgr12im  36133  imp5q  36335  elicc3  36340  areacirclem1  37737  areacirclem2  37738  areacirclem4  37740  areacirc  37742  filbcmb  37769  fzmul  37770  islshpcv  39076  cvrat3  39466  4atexlem7  40099  relexpmulg  43701  gneispacess2  44137  iunconnlem2  44926  fmtnoprmfac1  47546  fmtnoprmfac2  47548  fpprwppr  47720  grimgrtri  47928  usgrgrtrirex  47929  grlimgrtri  47975  itsclc0xyqsol  48715