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  20986  xrsdsreclblem  21195  matecl  22160  scmateALT  22247  riinopn  22643  neindisj2  22860  filufint  23657  tsmsxp  23892  ewlkle  29144  uspgr2wlkeq  29185  spthonepeq  29291  wwlksm1edg  29417  clwwisshclwws  29550  clwwlknwwlksn  29573  clwwlkinwwlk  29575  wwlksext2clwwlk  29592  3vfriswmgr  29813  homco1  31336  homulass  31337  hoadddir  31339  satffunlem  34705  mblfinlem3  36843  zerdivemp1x  37131  athgt  38643  psubspi  38934  paddasslem14  39020  eluzge0nn0  46331  iccpartigtl  46402  lighneal  46590  isomgrsym  46815