Theorem 3imp1 1348

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

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

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 1088

This theorem is referenced by:  3an1rs  1360  reupick2  4306  indcardi  10055  ledivge1le  13080  expcan  14187  ltexp2  14188  leexp1a  14193  expnbnd  14250  cshf1  14828  rtrclreclem4  15080  relexpindlem  15082  ncoprmlnprm  16747  rnglidlmcl  21177  xrsdsreclblem  21380  matecl  22363  scmateALT  22450  riinopn  22846  neindisj2  23061  filufint  23858  tsmsxp  24093  ewlkle  29585  uspgr2wlkeq  29626  spthonepeq  29734  wwlksm1edg  29863  clwwisshclwws  29996  clwwlknwwlksn  30019  clwwlkinwwlk  30021  wwlksext2clwwlk  30038  3vfriswmgr  30259  homco1  31782  homulass  31783  hoadddir  31785  satffunlem  35423  mblfinlem3  37683  zerdivemp1x  37971  athgt  39475  psubspi  39766  paddasslem14  39852  eluzge0nn0  47341  iccpartigtl  47437  lighneal  47625  uhgrimisgrgriclem  47943  uhgrimisgrgric  47944  clnbgrgrimlem  47946  uspgrlimlem3  48002  clnbgr3stgrgrlic  48024  gpgusgralem  48060