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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1088

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 210  df-an 400  df-3an 1090

This theorem is referenced by:  3an1rs  1360  reupick2  4219  indcardi  9554  ledivge1le  12556  expcan  13638  ltexp2  13639  leexp1a  13644  expnbnd  13698  cshf1  14274  rtrclreclem4  14523  relexpindlem  14525  ncoprmlnprm  16181  xrsdsreclblem  20276  matecl  21189  scmateALT  21276  riinopn  21672  neindisj2  21887  filufint  22684  tsmsxp  22919  ewlkle  27560  uspgr2wlkeq  27600  spthonepeq  27706  wwlksm1edg  27832  clwwisshclwws  27965  clwwlknwwlksn  27988  clwwlkinwwlk  27990  wwlksext2clwwlk  28007  3vfriswmgr  28228  homco1  29749  homulass  29750  hoadddir  29752  satffunlem  32947  mblfinlem3  35472  zerdivemp1x  35761  athgt  37126  psubspi  37417  paddasslem14  37503  eluzge0nn0  44386  iccpartigtl  44457  lighneal  44645  isomgrsym  44870