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  4282  indcardi  9935  ledivge1le  12966  expcan  14076  ltexp2  14077  leexp1a  14082  expnbnd  14139  cshf1  14716  rtrclreclem4  14968  relexpindlem  14970  ncoprmlnprm  16639  rnglidlmcl  21123  xrsdsreclblem  21319  matecl  22310  scmateALT  22397  riinopn  22793  neindisj2  23008  filufint  23805  tsmsxp  24040  ewlkle  29551  uspgr2wlkeq  29591  spthonepeq  29697  wwlksm1edg  29826  clwwisshclwws  29959  clwwlknwwlksn  29982  clwwlkinwwlk  29984  wwlksext2clwwlk  30001  3vfriswmgr  30222  homco1  31745  homulass  31746  hoadddir  31748  satffunlem  35374  mblfinlem3  37639  zerdivemp1x  37927  athgt  39435  psubspi  39726  paddasslem14  39812  eluzge0nn0  47296  iccpartigtl  47407  lighneal  47595  uhgrimisgrgriclem  47914  uhgrimisgrgric  47915  clnbgrgrimlem  47917  uspgrlimlem3  47974  clnbgr3stgrgrlic  48004  gpgusgralem  48040