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  4297  indcardi  10001  ledivge1le  13031  expcan  14141  ltexp2  14142  leexp1a  14147  expnbnd  14204  cshf1  14782  rtrclreclem4  15034  relexpindlem  15036  ncoprmlnprm  16705  rnglidlmcl  21133  xrsdsreclblem  21336  matecl  22319  scmateALT  22406  riinopn  22802  neindisj2  23017  filufint  23814  tsmsxp  24049  ewlkle  29540  uspgr2wlkeq  29581  spthonepeq  29689  wwlksm1edg  29818  clwwisshclwws  29951  clwwlknwwlksn  29974  clwwlkinwwlk  29976  wwlksext2clwwlk  29993  3vfriswmgr  30214  homco1  31737  homulass  31738  hoadddir  31740  satffunlem  35395  mblfinlem3  37660  zerdivemp1x  37948  athgt  39457  psubspi  39748  paddasslem14  39834  eluzge0nn0  47317  iccpartigtl  47428  lighneal  47616  uhgrimisgrgriclem  47934  uhgrimisgrgric  47935  clnbgrgrimlem  47937  uspgrlimlem3  47993  clnbgr3stgrgrlic  48015  gpgusgralem  48051