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  5590  oprabidw  7454  oprabid  7455  isinf  9235  infsupprpr  9476  axdc3lem4  10455  iccid  13435  difreicc  13529  fvf1tp  13842  relexpaddg  15116  issubg4  19243  rnglidlmcl  21378  reconn  25023  bcthlem2  25521  dvfsumrlim3  26229  ax5seg  29325  axcontlem4  29354  usgr2wlkneq  30142  frgrwopreg  30711  dfufd2lem  33870  cvmlift3lem4  35835  fscgr  36593  idinside  36597  brsegle  36621  seglecgr12im  36623  imp5q  36865  elicc3  36869  areacirclem1  38400  areacirclem2  38401  areacirclem4  38403  areacirc  38405  filbcmb  38432  fzmul  38433  islshpcv  39868  cvrat3  40257  4atexlem7  40890  relexpmulg  44477  gneispacess2  44913  iunconnlem2  45684  fmtnoprmfac1  48358  fmtnoprmfac2  48360  fpprwppr  48545  grimgrtri  48755  usgrgrtrirex  48756  grlimgrtri  48809  itsclc0xyqsol  49589