Theorem 3imp1 1354

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3an1rs  1366  reupick2  4259  indcardi  9954  ledivge1le  13006  expcan  14122  ltexp2  14123  leexp1a  14128  expnbnd  14185  cshf1  14763  rtrclreclem4  15014  relexpindlem  15016  ncoprmlnprm  16689  rnglidlmcl  21209  xrsdsreclblem  21388  matecl  22408  scmateALT  22495  riinopn  22891  neindisj2  23106  filufint  23903  tsmsxp  24138  ewlkle  29692  uspgr2wlkeq  29732  spthonepeq  29838  wwlksm1edg  29967  clwwisshclwws  30103  clwwlknwwlksn  30126  clwwlkinwwlk  30128  wwlksext2clwwlk  30145  3vfriswmgr  30366  homco1  31890  homulass  31891  hoadddir  31893  satffunlem  35629  mblfinlem3  38026  zerdivemp1x  38314  athgt  39948  psubspi  40239  paddasslem14  40325  eluzge0nn0  47775  iccpartigtl  47898  lighneal  48089  uhgrimisgrgriclem  48421  uhgrimisgrgric  48422  clnbgrgrimlem  48424  uspgrlimlem3  48481  clnbgr3stgrgrlic  48511  gpgusgralem  48547