Theorem 3impd 1344

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3imp2  1345  3impexp  1354  po2ne  5483  oprabidw  7181  oprabid  7182  wfrlem12  7960  isinf  8725  infsupprpr  8962  axdc3lem4  9869  iccid  12777  difreicc  12864  relexpaddg  14406  issubg4  18292  reconn  23430  bcthlem2  23922  dvfsumrlim3  24624  ax5seg  26718  axcontlem4  26747  usgr2wlkneq  27531  frgrwopreg  28096  cvmlift3lem4  32564  fscgr  33536  idinside  33540  brsegle  33564  seglecgr12im  33566  imp5q  33655  elicc3  33660  areacirclem1  34976  areacirclem2  34977  areacirclem4  34979  areacirc  34981  filbcmb  35009  fzmul  35010  islshpcv  36183  cvrat3  36572  4atexlem7  37205  relexpmulg  40048  gneispacess2  40489  iunconnlem2  41262  fmtnoprmfac1  43721  fmtnoprmfac2  43723  fpprwppr  43898  itsclc0xyqsol  44749