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

This theorem is referenced by:  3an1rs  1360  reupick2  4290  indcardi  9970  ledivge1le  13000  expcan  14110  ltexp2  14111  leexp1a  14116  expnbnd  14173  cshf1  14751  rtrclreclem4  15003  relexpindlem  15005  ncoprmlnprm  16674  rnglidlmcl  21102  xrsdsreclblem  21305  matecl  22288  scmateALT  22375  riinopn  22771  neindisj2  22986  filufint  23783  tsmsxp  24018  ewlkle  29509  uspgr2wlkeq  29549  spthonepeq  29655  wwlksm1edg  29784  clwwisshclwws  29917  clwwlknwwlksn  29940  clwwlkinwwlk  29942  wwlksext2clwwlk  29959  3vfriswmgr  30180  homco1  31703  homulass  31704  hoadddir  31706  satffunlem  35361  mblfinlem3  37626  zerdivemp1x  37914  athgt  39423  psubspi  39714  paddasslem14  39800  eluzge0nn0  47286  iccpartigtl  47397  lighneal  47585  uhgrimisgrgriclem  47903  uhgrimisgrgric  47904  clnbgrgrimlem  47906  uspgrlimlem3  47962  clnbgr3stgrgrlic  47984  gpgusgralem  48020