Theorem 3imp1 1404

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 1101	. 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  1414  reupick2  4021  indcardi  8977  ledivge1le  12015  expcan  13028  ltexp2  13029  leexp1a  13034  expnbnd  13108  cshf1  13677  rtrclreclem4  13921  relexpindlem  13923  ncoprmlnprm  15559  xrsdsreclblem  19915  matecl  20354  scmateALT  20441  riinopn  20836  neindisj2  21050  filufint  21846  tsmsxp  22080  ewlkle  26632  uspgr2wlkeq  26673  spthonepeq  26779  wwlksm1edg  26911  clwwisshclwws  27059  clwwlknwwlksn  27087  clwwlknwwlksnOLD  27088  clwwlkinwwlk  27090  wwlksext2clwwlk  27108  3vfriswmgr  27353  homco1  28890  homulass  28891  hoadddir  28893  mblfinlem3  33680  zerdivemp1x  33978  athgt  35162  psubspi  35453  paddasslem14  35539  eluzge0nn0  41749  iccpartigtl  41786  lighneal  41955