Theorem 3impd 1347

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3imp2  1348  3impexp  1357  po2ne  5542  oprabidw  7360  oprabid  7361  wfrlem12OLD  8213  isinf  9117  isinfOLD  9118  infsupprpr  9353  axdc3lem4  10302  iccid  13217  difreicc  13309  relexpaddg  14855  issubg4  18862  reconn  24089  bcthlem2  24587  dvfsumrlim3  25295  ax5seg  27536  axcontlem4  27565  usgr2wlkneq  28353  frgrwopreg  28916  cvmlift3lem4  33524  fscgr  34473  idinside  34477  brsegle  34501  seglecgr12im  34503  imp5q  34592  elicc3  34597  areacirclem1  35963  areacirclem2  35964  areacirclem4  35966  areacirc  35968  filbcmb  35996  fzmul  35997  islshpcv  37313  cvrat3  37703  4atexlem7  38336  relexpmulg  41628  gneispacess2  42066  iunconnlem2  42865  fmtnoprmfac1  45357  fmtnoprmfac2  45359  fpprwppr  45531  itsclc0xyqsol  46454