Theorem 3impd 1349

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3imp2  1350  3impexp  1359  po2ne  5547  oprabidw  7384  oprabid  7385  isinf  9165  isinfOLD  9166  infsupprpr  9415  axdc3lem4  10366  iccid  13311  difreicc  13405  fvf1tp  13711  relexpaddg  14978  issubg4  19042  rnglidlmcl  21141  reconn  24733  bcthlem2  25241  dvfsumrlim3  25956  ax5seg  28901  axcontlem4  28930  usgr2wlkneq  29719  frgrwopreg  30285  dfufd2lem  33499  cvmlift3lem4  35297  fscgr  36056  idinside  36060  brsegle  36084  seglecgr12im  36086  imp5q  36288  elicc3  36293  areacirclem1  37690  areacirclem2  37691  areacirclem4  37693  areacirc  37695  filbcmb  37722  fzmul  37723  islshpcv  39034  cvrat3  39424  4atexlem7  40057  relexpmulg  43686  gneispacess2  44122  iunconnlem2  44911  fmtnoprmfac1  47553  fmtnoprmfac2  47555  fpprwppr  47727  grimgrtri  47937  usgrgrtrirex  47938  grlimgrtri  47991  itsclc0xyqsol  48757