Theorem 3imp1 1349

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  3an1rs  1361  reupick2  4271  indcardi  9963  ledivge1le  13015  expcan  14131  ltexp2  14132  leexp1a  14137  expnbnd  14194  cshf1  14772  rtrclreclem4  15023  relexpindlem  15025  ncoprmlnprm  16698  rnglidlmcl  21214  xrsdsreclblem  21393  matecl  22390  scmateALT  22477  riinopn  22873  neindisj2  23088  filufint  23885  tsmsxp  24120  ewlkle  29674  uspgr2wlkeq  29714  spthonepeq  29820  wwlksm1edg  29949  clwwisshclwws  30085  clwwlknwwlksn  30108  clwwlkinwwlk  30110  wwlksext2clwwlk  30127  3vfriswmgr  30348  homco1  31872  homulass  31873  hoadddir  31875  satffunlem  35583  mblfinlem3  37980  zerdivemp1x  38268  athgt  39902  psubspi  40193  paddasslem14  40279  eluzge0nn0  47760  iccpartigtl  47883  lighneal  48074  uhgrimisgrgriclem  48406  uhgrimisgrgric  48407  clnbgrgrimlem  48409  uspgrlimlem3  48466  clnbgr3stgrgrlic  48496  gpgusgralem  48532