Theorem 3imp1 1366

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 1128	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 → 𝜏))
3	2	imp 412	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3an1rs  1378  reupick2  4284  indcardi  10041  ledivge1le  13105  expcan  14223  ltexp2  14224  leexp1a  14229  expnbnd  14286  cshf1  14871  rtrclreclem4  15122  relexpindlem  15124  ncoprmlnprm  16809  rnglidlmcl  21391  xrsdsreclblem  21613  matecl  22632  scmateALT  22719  riinopn  23115  neindisj2  23330  filufint  24128  tsmsxp  24363  ewlkle  30013  uspgr2wlkeq  30053  spthonepeq  30165  wwlksm1edg  30297  clwwisshclwws  30433  clwwlknwwlksn  30456  clwwlkinwwlk  30458  wwlksext2clwwlk  30475  3vfriswmgr  30700  homco1  32224  homulass  32225  hoadddir  32227  satffunlem  35930  mblfinlem3  38367  zerdivemp1x  38656  athgt  40288  psubspi  40579  paddasslem14  40665  eluzge0nn0  48107  iccpartigtl  48230  lighneal  48421  uhgrimisgrgriclem  48753  uhgrimisgrgric  48754  clnbgrgrimlem  48756  uspgrlimlem3  48813  clnbgr3stgrgrlic  48843  gpgusgralem  48879