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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3an1rs  1378  reupick2  4275  indcardi  10125  ledivge1le  13198  expcan  14317  ltexp2  14318  leexp1a  14323  expnbnd  14381  cshf1  14967  rtrclreclem4  15221  relexpindlem  15223  ncoprmlnprm  16911  rnglidlmcl  21502  xrsdsreclblem  21726  matecl  22747  scmateALT  22834  riinopn  23233  neindisj2  23448  filufint  24246  tsmsxp  24481  ewlkle  30193  uspgr2wlkeq  30233  spthonepeq  30345  wwlksm1edg  30477  clwwisshclwws  30613  clwwlknwwlksn  30636  clwwlkinwwlk  30638  wwlksext2clwwlk  30655  3vfriswmgr  30886  homco1  32410  homulass  32411  hoadddir  32413  satffunlem  36254  mblfinlem3  38684  zerdivemp1x  38988  athgt  40620  psubspi  40911  paddasslem14  40997  eluzge0nn0  48489  iccpartigtl  48612  lighneal  48803  uhgrimisgrgriclem  49135  uhgrimisgrgric  49136  clnbgrgrimlem  49138  uspgrlimlem3  49195  clnbgr3stgrgrlic  49225  gpgusgralem  49261