Theorem 3imp1 1347

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

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

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

This theorem is referenced by:  3an1rs  1359  reupick2  4350  indcardi  10110  ledivge1le  13128  expcan  14219  ltexp2  14220  leexp1a  14225  expnbnd  14281  cshf1  14858  rtrclreclem4  15110  relexpindlem  15112  ncoprmlnprm  16775  rnglidlmcl  21249  xrsdsreclblem  21453  matecl  22452  scmateALT  22539  riinopn  22935  neindisj2  23152  filufint  23949  tsmsxp  24184  ewlkle  29641  uspgr2wlkeq  29682  spthonepeq  29788  wwlksm1edg  29914  clwwisshclwws  30047  clwwlknwwlksn  30070  clwwlkinwwlk  30072  wwlksext2clwwlk  30089  3vfriswmgr  30310  homco1  31833  homulass  31834  hoadddir  31836  satffunlem  35369  mblfinlem3  37619  zerdivemp1x  37907  athgt  39413  psubspi  39704  paddasslem14  39790  eluzge0nn0  47227  iccpartigtl  47297  lighneal  47485  uhgrimisgrgriclem  47782  uhgrimisgrgric  47783  clnbgrgrimlem  47785  uspgrlimlem3  47814