Theorem 3impd 1350

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  1351  3impexp  1360  po2ne  5555  oprabidw  7398  oprabid  7399  isinf  9175  infsupprpr  9419  axdc3lem4  10375  iccid  13343  difreicc  13437  fvf1tp  13748  relexpaddg  15015  issubg4  19121  rnglidlmcl  21214  reconn  24794  bcthlem2  25292  dvfsumrlim3  26000  ax5seg  29007  axcontlem4  29036  usgr2wlkneq  29824  frgrwopreg  30393  dfufd2lem  33609  cvmlift3lem4  35504  fscgr  36262  idinside  36266  brsegle  36290  seglecgr12im  36292  imp5q  36494  elicc3  36499  areacirclem1  38029  areacirclem2  38030  areacirclem4  38032  areacirc  38034  filbcmb  38061  fzmul  38062  islshpcv  39499  cvrat3  39888  4atexlem7  40521  relexpmulg  44137  gneispacess2  44573  iunconnlem2  45361  fmtnoprmfac1  48028  fmtnoprmfac2  48030  fpprwppr  48215  grimgrtri  48425  usgrgrtrirex  48426  grlimgrtri  48479  itsclc0xyqsol  49244