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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  3imp2  1350  3impexp  1359  po2ne  5608  oprabidw  7462  oprabid  7463  wfrlem12OLD  8360  isinf  9296  isinfOLD  9297  infsupprpr  9544  axdc3lem4  10493  iccid  13432  difreicc  13524  fvf1tp  13829  relexpaddg  15092  issubg4  19163  rnglidlmcl  21226  reconn  24850  bcthlem2  25359  dvfsumrlim3  26074  ax5seg  28953  axcontlem4  28982  usgr2wlkneq  29776  frgrwopreg  30342  dfufd2lem  33577  cvmlift3lem4  35327  fscgr  36081  idinside  36085  brsegle  36109  seglecgr12im  36111  imp5q  36313  elicc3  36318  areacirclem1  37715  areacirclem2  37716  areacirclem4  37718  areacirc  37720  filbcmb  37747  fzmul  37748  islshpcv  39054  cvrat3  39444  4atexlem7  40077  relexpmulg  43723  gneispacess2  44159  iunconnlem2  44955  fmtnoprmfac1  47552  fmtnoprmfac2  47554  fpprwppr  47726  grimgrtri  47916  usgrgrtrirex  47917  grlimgrtri  47963  itsclc0xyqsol  48689