Theorem 3impd 1303

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

Syntax hints:   → wi 4   ∧ w3a 1054

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 197  df-an 385  df-3an 1056

This theorem is referenced by:  3imp2  1304  3impexp  1311  oprabid  6717  wfrlem12  7471  isinf  8214  axdc3lem4  9313  iccid  12258  difreicc  12342  relexpaddg  13837  issubg4  17660  reconn  22678  bcthlem2  23168  dvfsumrlim3  23841  ax5seg  25863  axcontlem4  25892  usgr2wlkneq  26708  frgrwopreg  27303  cvmlift3lem4  31430  fscgr  32312  idinside  32316  brsegle  32340  seglecgr12im  32342  imp5q  32431  elicc3  32436  areacirclem1  33630  areacirclem2  33631  areacirclem4  33633  areacirc  33635  filbcmb  33665  fzmul  33667  islshpcv  34658  cvrat3  35046  4atexlem7  35679  relexpmulg  38319  gneispacess2  38761  iunconnlem2  39485  fmtnoprmfac1  41802  fmtnoprmfac2  41804