Theorem 3imp1 1280

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 386  df-3an 1039

This theorem is referenced by:  reupick2  3913  indcardi  8864  ledivge1le  11901  expcan  12913  ltexp2  12914  leexp1a  12919  expnbnd  12993  cshf1  13556  rtrclreclem4  13801  relexpindlem  13803  ncoprmlnprm  15436  xrsdsreclblem  19792  matecl  20231  scmateALT  20318  riinopn  20713  neindisj2  20927  filufint  21724  tsmsxp  21958  ewlkle  26501  uspgr2wlkeq  26542  spthonepeq  26648  wwlksm1edg  26767  clwwlkinwwlk  26905  clwwisshclwws  26928  3vfriswmgr  27142  clwwlksnwwlksn  27209  homco1  28660  homulass  28661  hoadddir  28663  mblfinlem3  33448  zerdivemp1x  33746  athgt  34742  psubspi  35033  paddasslem14  35119  eluzge0nn0  41322  iccpartigtl  41359  lighneal  41528