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  5575  oprabidw  7449  oprabid  7450  isinf  9249  infsupprpr  9491  axdc3lem4  10524  iccid  13514  difreicc  13608  fvf1tp  13922  relexpaddg  15199  issubg4  19349  rnglidlmcl  21488  reconn  25141  bcthlem2  25639  dvfsumrlim3  26346  ax5seg  29509  axcontlem4  29538  usgr2wlkneq  30335  frgrwopreg  30917  dfufd2lem  34074  cvmlift3lem4  36066  fscgr  36825  idinside  36829  brsegle  36853  seglecgr12im  36855  imp5q  37081  elicc3  37085  areacirclem1  38606  areacirclem2  38607  areacirclem4  38609  areacirc  38611  filbcmb  38654  fzmul  38655  islshpcv  40090  cvrat3  40479  4atexlem7  41112  relexpmulg  44695  gneispacess2  45131  iunconnlem2  45902  fmtnoprmfac1  48619  fmtnoprmfac2  48621  fpprwppr  48806  grimgrtri  49016  usgrgrtrirex  49017  grlimgrtri  49070  itsclc0xyqsol  49849