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  5538  oprabidw  7377  oprabid  7378  isinf  9149  infsupprpr  9390  axdc3lem4  10344  iccid  13290  difreicc  13384  fvf1tp  13693  relexpaddg  14960  issubg4  19058  rnglidlmcl  21153  reconn  24744  bcthlem2  25252  dvfsumrlim3  25967  ax5seg  28916  axcontlem4  28945  usgr2wlkneq  29734  frgrwopreg  30303  dfufd2lem  33514  cvmlift3lem4  35366  fscgr  36124  idinside  36128  brsegle  36152  seglecgr12im  36154  imp5q  36356  elicc3  36361  areacirclem1  37747  areacirclem2  37748  areacirclem4  37750  areacirc  37752  filbcmb  37779  fzmul  37780  islshpcv  39151  cvrat3  39540  4atexlem7  40173  relexpmulg  43802  gneispacess2  44238  iunconnlem2  45026  fmtnoprmfac1  47664  fmtnoprmfac2  47666  fpprwppr  47838  grimgrtri  48048  usgrgrtrirex  48049  grlimgrtri  48102  itsclc0xyqsol  48868