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  4277  indcardi  10113  ledivge1le  13186  expcan  14305  ltexp2  14306  leexp1a  14311  expnbnd  14369  cshf1  14954  rtrclreclem4  15207  relexpindlem  15209  ncoprmlnprm  16897  rnglidlmcl  21488  xrsdsreclblem  21712  matecl  22733  scmateALT  22820  riinopn  23219  neindisj2  23434  filufint  24232  tsmsxp  24467  ewlkle  30179  uspgr2wlkeq  30219  spthonepeq  30331  wwlksm1edg  30463  clwwisshclwws  30599  clwwlknwwlksn  30622  clwwlkinwwlk  30624  wwlksext2clwwlk  30641  3vfriswmgr  30872  homco1  32396  homulass  32397  hoadddir  32399  satffunlem  36145  mblfinlem3  38557  zerdivemp1x  38861  athgt  40493  psubspi  40784  paddasslem14  40870  eluzge0nn0  48351  iccpartigtl  48474  lighneal  48665  uhgrimisgrgriclem  48997  uhgrimisgrgric  48998  clnbgrgrimlem  49000  uspgrlimlem3  49057  clnbgr3stgrgrlic  49087  gpgusgralem  49123