Theorem 3imp1 1366

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  3an1rs  1378  reupick2  4284  indcardi  10021  ledivge1le  13084  expcan  14201  ltexp2  14202  leexp1a  14207  expnbnd  14264  cshf1  14843  rtrclreclem4  15094  relexpindlem  15096  ncoprmlnprm  16782  rnglidlmcl  21341  xrsdsreclblem  21563  matecl  22582  scmateALT  22669  riinopn  23065  neindisj2  23280  filufint  24077  tsmsxp  24312  ewlkle  29955  uspgr2wlkeq  29995  spthonepeq  30101  wwlksm1edg  30230  clwwisshclwws  30366  clwwlknwwlksn  30389  clwwlkinwwlk  30391  wwlksext2clwwlk  30408  3vfriswmgr  30629  homco1  32153  homulass  32154  hoadddir  32156  satffunlem  35893  mblfinlem3  38310  zerdivemp1x  38598  athgt  40230  psubspi  40521  paddasslem14  40607  eluzge0nn0  48049  iccpartigtl  48172  lighneal  48363  uhgrimisgrgriclem  48695  uhgrimisgrgric  48696  clnbgrgrimlem  48698  uspgrlimlem3  48755  clnbgr3stgrgrlic  48785  gpgusgralem  48821