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  5489  oprabidw  7187  oprabid  7188  wfrlem12  7966  isinf  8731  infsupprpr  8968  axdc3lem4  9875  iccid  12784  difreicc  12871  relexpaddg  14412  issubg4  18298  reconn  23436  bcthlem2  23928  dvfsumrlim3  24630  ax5seg  26724  axcontlem4  26753  usgr2wlkneq  27537  frgrwopreg  28102  cvmlift3lem4  32569  fscgr  33541  idinside  33545  brsegle  33569  seglecgr12im  33571  imp5q  33660  elicc3  33665  areacirclem1  34997  areacirclem2  34998  areacirclem4  35000  areacirc  35002  filbcmb  35030  fzmul  35031  islshpcv  36204  cvrat3  36593  4atexlem7  37226  relexpmulg  40075  gneispacess2  40516  iunconnlem2  41289  fmtnoprmfac1  43747  fmtnoprmfac2  43749  fpprwppr  43924  itsclc0xyqsol  44775