Theorem 3imp1 1366

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3an1rs  1378  reupick2  4279  indcardi  10159  ledivge1le  13233  expcan  14352  ltexp2  14353  leexp1a  14358  expnbnd  14417  cshf1  15003  rtrclreclem4  15257  relexpindlem  15259  ncoprmlnprm  16948  rnglidlmcl  21546  xrsdsreclblem  21771  matecl  22795  scmateALT  22882  riinopn  23281  neindisj2  23496  filufint  24294  tsmsxp  24529  ewlkle  30243  uspgr2wlkeq  30283  spthonepeq  30395  wwlksm1edg  30527  clwwisshclwws  30663  clwwlknwwlksn  30686  clwwlkinwwlk  30688  wwlksext2clwwlk  30705  3vfriswmgr  30936  homco1  32460  homulass  32461  hoadddir  32463  satffunlem  36374  mblfinlem3  38845  zerdivemp1x  39147  athgt  40779  psubspi  41070  paddasslem14  41156  eluzge0nn0  48655  iccpartigtl  48778  lighneal  48969  uhgrimisgrgriclem  49301  uhgrimisgrgric  49302  clnbgrgrimlem  49304  uspgrlimlem3  49361  clnbgr3stgrgrlic  49391  gpgusgralem  49427