Theorem 3imp1 1346

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 206  df-an 396  df-3an 1088

This theorem is referenced by:  3an1rs  1358  reupick2  4320  indcardi  10042  ledivge1le  13052  expcan  14141  ltexp2  14142  leexp1a  14147  expnbnd  14202  cshf1  14767  rtrclreclem4  15015  relexpindlem  15017  ncoprmlnprm  16671  rnglidlmcl  21070  xrsdsreclblem  21279  matecl  22246  scmateALT  22333  riinopn  22729  neindisj2  22946  filufint  23743  tsmsxp  23978  ewlkle  29294  uspgr2wlkeq  29335  spthonepeq  29441  wwlksm1edg  29567  clwwisshclwws  29700  clwwlknwwlksn  29723  clwwlkinwwlk  29725  wwlksext2clwwlk  29742  3vfriswmgr  29963  homco1  31486  homulass  31487  hoadddir  31489  satffunlem  34855  mblfinlem3  36990  zerdivemp1x  37278  athgt  38790  psubspi  39081  paddasslem14  39167  eluzge0nn0  46478  iccpartigtl  46549  lighneal  46737  isomgrsym  46962