Theorem 3impd 1365

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3imp2  1366  3impexp  1375  po2ne  5575  oprabidw  7431  oprabid  7432  isinf  9213  infsupprpr  9454  axdc3lem4  10425  iccid  13405  difreicc  13499  fvf1tp  13810  relexpaddg  15078  issubg4  19200  rnglidlmcl  21307  reconn  24943  bcthlem2  25441  dvfsumrlim3  26149  ax5seg  29193  axcontlem4  29222  usgr2wlkneq  30010  frgrwopreg  30579  dfufd2lem  33751  cvmlift3lem4  35680  fscgr  36438  idinside  36442  brsegle  36466  seglecgr12im  36468  imp5q  36680  elicc3  36685  areacirclem1  38214  areacirclem2  38215  areacirclem4  38217  areacirc  38219  filbcmb  38246  fzmul  38247  islshpcv  39684  cvrat3  40073  4atexlem7  40706  relexpmulg  44293  gneispacess2  44729  iunconnlem2  45502  fmtnoprmfac1  48173  fmtnoprmfac2  48175  fpprwppr  48360  grimgrtri  48570  usgrgrtrirex  48571  grlimgrtri  48624  itsclc0xyqsol  49400