Theorem 3impd 1367

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3imp2  1368  3impexp  1377  po2ne  5579  oprabidw  7444  oprabid  7445  isinf  9235  infsupprpr  9476  axdc3lem4  10455  iccid  13443  difreicc  13537  fvf1tp  13850  relexpaddg  15126  issubg4  19269  rnglidlmcl  21404  reconn  25055  bcthlem2  25553  dvfsumrlim3  26260  ax5seg  29395  axcontlem4  29424  usgr2wlkneq  30221  frgrwopreg  30803  dfufd2lem  33959  cvmlift3lem4  35901  fscgr  36660  idinside  36664  brsegle  36688  seglecgr12im  36690  imp5q  36932  elicc3  36936  areacirclem1  38457  areacirclem2  38458  areacirclem4  38460  areacirc  38462  filbcmb  38490  fzmul  38491  islshpcv  39926  cvrat3  40315  4atexlem7  40948  relexpmulg  44550  gneispacess2  44986  iunconnlem2  45757  fmtnoprmfac1  48468  fmtnoprmfac2  48470  fpprwppr  48655  grimgrtri  48865  usgrgrtrirex  48866  grlimgrtri  48919  itsclc0xyqsol  49698