Theorem 3impd 1355

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3imp2  1356  3impexp  1365  po2ne  5549  oprabidw  7394  oprabid  7395  isinf  9172  infsupprpr  9416  axdc3lem4  10373  iccid  13341  difreicc  13435  fvf1tp  13746  relexpaddg  15013  issubg4  19119  rnglidlmcl  21216  reconn  24819  bcthlem2  25317  dvfsumrlim3  26025  ax5seg  29032  axcontlem4  29061  usgr2wlkneq  29849  frgrwopreg  30418  dfufd2lem  33639  cvmlift3lem4  35557  fscgr  36315  idinside  36319  brsegle  36343  seglecgr12im  36345  imp5q  36547  elicc3  36552  areacirclem1  38082  areacirclem2  38083  areacirclem4  38085  areacirc  38087  filbcmb  38114  fzmul  38115  islshpcv  39552  cvrat3  39941  4atexlem7  40574  relexpmulg  44161  gneispacess2  44597  iunconnlem2  45385  fmtnoprmfac1  48050  fmtnoprmfac2  48052  fpprwppr  48237  grimgrtri  48447  usgrgrtrirex  48448  grlimgrtri  48501  itsclc0xyqsol  49266