Theorem 3imp1 1349

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

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

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 1089

This theorem is referenced by:  3an1rs  1361  reupick2  4272  indcardi  9952  ledivge1le  12979  expcan  14093  ltexp2  14094  leexp1a  14099  expnbnd  14156  cshf1  14734  rtrclreclem4  14985  relexpindlem  14987  ncoprmlnprm  16656  rnglidlmcl  21173  xrsdsreclblem  21369  matecl  22368  scmateALT  22455  riinopn  22851  neindisj2  23066  filufint  23863  tsmsxp  24098  ewlkle  29663  uspgr2wlkeq  29703  spthonepeq  29809  wwlksm1edg  29938  clwwisshclwws  30074  clwwlknwwlksn  30097  clwwlkinwwlk  30099  wwlksext2clwwlk  30116  3vfriswmgr  30337  homco1  31861  homulass  31862  hoadddir  31864  satffunlem  35589  mblfinlem3  37971  zerdivemp1x  38259  athgt  39893  psubspi  40184  paddasslem14  40270  eluzge0nn0  47746  iccpartigtl  47857  lighneal  48045  uhgrimisgrgriclem  48364  uhgrimisgrgric  48365  clnbgrgrimlem  48367  uspgrlimlem3  48424  clnbgr3stgrgrlic  48454  gpgusgralem  48490