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

Syntax hints:   → wi 4   ∧ w3a 1089

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 400  df-3an 1091

This theorem is referenced by:  3imp2  1351  3impexp  1360  po2ne  5469  oprabidw  7222  oprabid  7223  wfrlem12  8044  isinf  8867  infsupprpr  9098  axdc3lem4  10032  iccid  12945  difreicc  13037  relexpaddg  14581  issubg4  18516  reconn  23679  bcthlem2  24176  dvfsumrlim3  24884  ax5seg  26983  axcontlem4  27012  usgr2wlkneq  27797  frgrwopreg  28360  cvmlift3lem4  32951  fscgr  34068  idinside  34072  brsegle  34096  seglecgr12im  34098  imp5q  34187  elicc3  34192  areacirclem1  35551  areacirclem2  35552  areacirclem4  35554  areacirc  35556  filbcmb  35584  fzmul  35585  islshpcv  36753  cvrat3  37142  4atexlem7  37775  relexpmulg  40936  gneispacess2  41374  iunconnlem2  42169  fmtnoprmfac1  44633  fmtnoprmfac2  44635  fpprwppr  44807  itsclc0xyqsol  45730