Theorem 3imp1 1345

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  3an1rs  1357  reupick2  4251  indcardi  9728  ledivge1le  12730  expcan  13815  ltexp2  13816  leexp1a  13821  expnbnd  13875  cshf1  14451  rtrclreclem4  14700  relexpindlem  14702  ncoprmlnprm  16360  xrsdsreclblem  20556  matecl  21482  scmateALT  21569  riinopn  21965  neindisj2  22182  filufint  22979  tsmsxp  23214  ewlkle  27875  uspgr2wlkeq  27915  spthonepeq  28021  wwlksm1edg  28147  clwwisshclwws  28280  clwwlknwwlksn  28303  clwwlkinwwlk  28305  wwlksext2clwwlk  28322  3vfriswmgr  28543  homco1  30064  homulass  30065  hoadddir  30067  satffunlem  33263  mblfinlem3  35743  zerdivemp1x  36032  athgt  37397  psubspi  37688  paddasslem14  37774  eluzge0nn0  44692  iccpartigtl  44763  lighneal  44951  isomgrsym  45176