Theorem 3imp1 1361

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1098

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 209  df-an 400  df-3an 1100

This theorem is referenced by:  3an1rs  1373  reupick2  4283  indcardi  9997  ledivge1le  13066  expcan  14182  ltexp2  14183  leexp1a  14188  expnbnd  14245  cshf1  14823  rtrclreclem4  15074  relexpindlem  15076  ncoprmlnprm  16763  rnglidlmcl  21283  xrsdsreclblem  21462  matecl  22482  scmateALT  22569  riinopn  22965  neindisj2  23180  filufint  23977  tsmsxp  24212  ewlkle  29803  uspgr2wlkeq  29843  spthonepeq  29949  wwlksm1edg  30078  clwwisshclwws  30214  clwwlknwwlksn  30237  clwwlkinwwlk  30239  wwlksext2clwwlk  30256  3vfriswmgr  30477  homco1  32001  homulass  32002  hoadddir  32004  satffunlem  35748  mblfinlem3  38155  zerdivemp1x  38443  athgt  40077  psubspi  40368  paddasslem14  40454  eluzge0nn0  47903  iccpartigtl  48026  lighneal  48217  uhgrimisgrgriclem  48549  uhgrimisgrgric  48550  clnbgrgrimlem  48552  uspgrlimlem3  48609  clnbgr3stgrgrlic  48639  gpgusgralem  48675