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  4283  indcardi  9951  ledivge1le  12978  expcan  14092  ltexp2  14093  leexp1a  14098  expnbnd  14155  cshf1  14733  rtrclreclem4  14984  relexpindlem  14986  ncoprmlnprm  16655  rnglidlmcl  21171  xrsdsreclblem  21367  matecl  22369  scmateALT  22456  riinopn  22852  neindisj2  23067  filufint  23864  tsmsxp  24099  ewlkle  29679  uspgr2wlkeq  29719  spthonepeq  29825  wwlksm1edg  29954  clwwisshclwws  30090  clwwlknwwlksn  30113  clwwlkinwwlk  30115  wwlksext2clwwlk  30132  3vfriswmgr  30353  homco1  31876  homulass  31877  hoadddir  31879  satffunlem  35595  mblfinlem3  37860  zerdivemp1x  38148  athgt  39716  psubspi  40007  paddasslem14  40093  eluzge0nn0  47558  iccpartigtl  47669  lighneal  47857  uhgrimisgrgriclem  48176  uhgrimisgrgric  48177  clnbgrgrimlem  48179  uspgrlimlem3  48236  clnbgr3stgrgrlic  48266  gpgusgralem  48302