Theorem 3imp1 1346

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 407	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3an1rs  1358  reupick2  4254  indcardi  9797  ledivge1le  12801  expcan  13887  ltexp2  13888  leexp1a  13893  expnbnd  13947  cshf1  14523  rtrclreclem4  14772  relexpindlem  14774  ncoprmlnprm  16432  xrsdsreclblem  20644  matecl  21574  scmateALT  21661  riinopn  22057  neindisj2  22274  filufint  23071  tsmsxp  23306  ewlkle  27972  uspgr2wlkeq  28013  spthonepeq  28120  wwlksm1edg  28246  clwwisshclwws  28379  clwwlknwwlksn  28402  clwwlkinwwlk  28404  wwlksext2clwwlk  28421  3vfriswmgr  28642  homco1  30163  homulass  30164  hoadddir  30166  satffunlem  33363  mblfinlem3  35816  zerdivemp1x  36105  athgt  37470  psubspi  37761  paddasslem14  37847  eluzge0nn0  44804  iccpartigtl  44875  lighneal  45063  isomgrsym  45288