Theorem 3imp1 1441

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  3an1rs  1453  reupick2  4056  indcardi  9074  ledivge1le  12114  expcan  13127  ltexp2  13128  leexp1a  13133  expnbnd  13207  cshf1  13776  rtrclreclem4  14020  relexpindlem  14022  ncoprmlnprm  15658  xrsdsreclblem  20014  matecl  20453  scmateALT  20540  riinopn  20935  neindisj2  21149  filufint  21945  tsmsxp  22179  ewlkle  26732  uspgr2wlkeq  26773  spthonepeq  26879  wwlksm1edg  27011  clwwisshclwws  27159  clwwlknwwlksn  27187  clwwlknwwlksnOLD  27188  clwwlkinwwlk  27190  wwlksext2clwwlk  27208  3vfriswmgr  27453  homco1  28990  homulass  28991  hoadddir  28993  mblfinlem3  33779  zerdivemp1x  34077  athgt  35263  psubspi  35554  paddasslem14  35640  eluzge0nn0  41850  iccpartigtl  41887  lighneal  42056