Theorem 3imp1 1345

Description: Importation to left triple conjunction. (Contributed by NM, 24-Feb-2005.)

Hypothesis

Ref	Expression
3imp1.1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Assertion

Ref	Expression
3imp1	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Proof of Theorem 3imp1

Step	Hyp	Ref	Expression
1		3imp1.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2	1	3imp 1109	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 → 𝜏))
3	2	imp 405	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 206  df-an 395  df-3an 1087

This theorem is referenced by:  3an1rs  1357  reupick2  4321  indcardi  10040  ledivge1le  13051  expcan  14140  ltexp2  14141  leexp1a  14146  expnbnd  14201  cshf1  14766  rtrclreclem4  15014  relexpindlem  15016  ncoprmlnprm  16670  rnglidlmcl  20984  xrsdsreclblem  21193  matecl  22149  scmateALT  22236  riinopn  22632  neindisj2  22849  filufint  23646  tsmsxp  23881  ewlkle  29127  uspgr2wlkeq  29168  spthonepeq  29274  wwlksm1edg  29400  clwwisshclwws  29533  clwwlknwwlksn  29556  clwwlkinwwlk  29558  wwlksext2clwwlk  29575  3vfriswmgr  29796  homco1  31319  homulass  31320  hoadddir  31322  satffunlem  34688  mblfinlem3  36832  zerdivemp1x  37120  athgt  38632  psubspi  38923  paddasslem14  39009  eluzge0nn0  46320  iccpartigtl  46391  lighneal  46579  isomgrsym  46804