Theorem 3imp1 1349

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  3an1rs  1361  reupick2  4285  indcardi  9963  ledivge1le  12990  expcan  14104  ltexp2  14105  leexp1a  14110  expnbnd  14167  cshf1  14745  rtrclreclem4  14996  relexpindlem  14998  ncoprmlnprm  16667  rnglidlmcl  21183  xrsdsreclblem  21379  matecl  22381  scmateALT  22468  riinopn  22864  neindisj2  23079  filufint  23876  tsmsxp  24111  ewlkle  29691  uspgr2wlkeq  29731  spthonepeq  29837  wwlksm1edg  29966  clwwisshclwws  30102  clwwlknwwlksn  30125  clwwlkinwwlk  30127  wwlksext2clwwlk  30144  3vfriswmgr  30365  homco1  31889  homulass  31890  hoadddir  31892  satffunlem  35617  mblfinlem3  37910  zerdivemp1x  38198  athgt  39832  psubspi  40123  paddasslem14  40209  eluzge0nn0  47672  iccpartigtl  47783  lighneal  47971  uhgrimisgrgriclem  48290  uhgrimisgrgric  48291  clnbgrgrimlem  48293  uspgrlimlem3  48350  clnbgr3stgrgrlic  48380  gpgusgralem  48416