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  4277  indcardi  10044  ledivge1le  13115  expcan  14233  ltexp2  14234  leexp1a  14239  expnbnd  14296  cshf1  14881  rtrclreclem4  15134  relexpindlem  15136  ncoprmlnprm  16819  rnglidlmcl  21404  xrsdsreclblem  21626  matecl  22647  scmateALT  22734  riinopn  23133  neindisj2  23348  filufint  24146  tsmsxp  24381  ewlkle  30065  uspgr2wlkeq  30105  spthonepeq  30217  wwlksm1edg  30349  clwwisshclwws  30485  clwwlknwwlksn  30508  clwwlkinwwlk  30510  wwlksext2clwwlk  30527  3vfriswmgr  30758  homco1  32282  homulass  32283  hoadddir  32285  satffunlem  35980  mblfinlem3  38408  zerdivemp1x  38697  athgt  40329  psubspi  40620  paddasslem14  40706  eluzge0nn0  48200  iccpartigtl  48323  lighneal  48514  uhgrimisgrgriclem  48846  uhgrimisgrgric  48847  clnbgrgrimlem  48849  uspgrlimlem3  48906  clnbgr3stgrgrlic  48936  gpgusgralem  48972