Theorem 3imp1 1348

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

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

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 1088

This theorem is referenced by:  3an1rs  1360  reupick2  4276  indcardi  9927  ledivge1le  12958  expcan  14071  ltexp2  14072  leexp1a  14077  expnbnd  14134  cshf1  14712  rtrclreclem4  14963  relexpindlem  14965  ncoprmlnprm  16634  rnglidlmcl  21148  xrsdsreclblem  21344  matecl  22335  scmateALT  22422  riinopn  22818  neindisj2  23033  filufint  23830  tsmsxp  24065  ewlkle  29579  uspgr2wlkeq  29619  spthonepeq  29725  wwlksm1edg  29854  clwwisshclwws  29987  clwwlknwwlksn  30010  clwwlkinwwlk  30012  wwlksext2clwwlk  30029  3vfriswmgr  30250  homco1  31773  homulass  31774  hoadddir  31776  satffunlem  35437  mblfinlem3  37699  zerdivemp1x  37987  athgt  39495  psubspi  39786  paddasslem14  39872  eluzge0nn0  47343  iccpartigtl  47454  lighneal  47642  uhgrimisgrgriclem  47961  uhgrimisgrgric  47962  clnbgrgrimlem  47964  uspgrlimlem3  48021  clnbgr3stgrgrlic  48051  gpgusgralem  48087