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  5574  oprabidw  7452  oprabid  7453  isinf  9260  infsupprpr  9502  axdc3lem4  10535  iccid  13525  difreicc  13619  fvf1tp  13933  relexpaddg  15212  issubg4  19362  rnglidlmcl  21501  reconn  25154  bcthlem2  25652  dvfsumrlim3  26359  ax5seg  29522  axcontlem4  29551  usgr2wlkneq  30348  frgrwopreg  30930  dfufd2lem  34128  cvmlift3lem4  36174  fscgr  36938  idinside  36942  brsegle  36966  seglecgr12im  36968  imp5q  37194  elicc3  37198  areacirclem1  38720  areacirclem2  38721  areacirclem4  38723  areacirc  38725  filbcmb  38768  fzmul  38769  islshpcv  40204  cvrat3  40593  4atexlem7  41226  relexpmulg  44804  gneispacess2  45240  iunconnlem2  46011  fmtnoprmfac1  48744  fmtnoprmfac2  48746  fpprwppr  48931  grimgrtri  49141  usgrgrtrirex  49142  grlimgrtri  49195  itsclc0xyqsol  49974