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  5548  oprabidw  7389  oprabid  7390  isinf  9165  infsupprpr  9409  axdc3lem4  10363  iccid  13306  difreicc  13400  fvf1tp  13709  relexpaddg  14976  issubg4  19075  rnglidlmcl  21171  reconn  24773  bcthlem2  25281  dvfsumrlim3  25996  ax5seg  29011  axcontlem4  29040  usgr2wlkneq  29829  frgrwopreg  30398  dfufd2lem  33630  cvmlift3lem4  35516  fscgr  36274  idinside  36278  brsegle  36302  seglecgr12im  36304  imp5q  36506  elicc3  36511  areacirclem1  37909  areacirclem2  37910  areacirclem4  37912  areacirc  37914  filbcmb  37941  fzmul  37942  islshpcv  39313  cvrat3  39702  4atexlem7  40335  relexpmulg  43951  gneispacess2  44387  iunconnlem2  45175  fmtnoprmfac1  47811  fmtnoprmfac2  47813  fpprwppr  47985  grimgrtri  48195  usgrgrtrirex  48196  grlimgrtri  48249  itsclc0xyqsol  49014