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  4272  indcardi  9954  ledivge1le  13006  expcan  14122  ltexp2  14123  leexp1a  14128  expnbnd  14185  cshf1  14763  rtrclreclem4  15014  relexpindlem  15016  ncoprmlnprm  16689  rnglidlmcl  21206  xrsdsreclblem  21402  matecl  22400  scmateALT  22487  riinopn  22883  neindisj2  23098  filufint  23895  tsmsxp  24130  ewlkle  29689  uspgr2wlkeq  29729  spthonepeq  29835  wwlksm1edg  29964  clwwisshclwws  30100  clwwlknwwlksn  30123  clwwlkinwwlk  30125  wwlksext2clwwlk  30142  3vfriswmgr  30363  homco1  31887  homulass  31888  hoadddir  31890  satffunlem  35599  mblfinlem3  37994  zerdivemp1x  38282  athgt  39916  psubspi  40207  paddasslem14  40293  eluzge0nn0  47772  iccpartigtl  47895  lighneal  48086  uhgrimisgrgriclem  48418  uhgrimisgrgric  48419  clnbgrgrimlem  48421  uspgrlimlem3  48478  clnbgr3stgrgrlic  48508  gpgusgralem  48544