Theorem 3imp1 1343

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3an1rs  1355  reupick2  4291  indcardi  9469  ledivge1le  12463  expcan  13536  ltexp2  13537  leexp1a  13542  expnbnd  13596  cshf1  14174  rtrclreclem4  14422  relexpindlem  14424  ncoprmlnprm  16070  xrsdsreclblem  20593  matecl  21036  scmateALT  21123  riinopn  21518  neindisj2  21733  filufint  22530  tsmsxp  22765  ewlkle  27389  uspgr2wlkeq  27429  spthonepeq  27535  wwlksm1edg  27661  clwwisshclwws  27795  clwwlknwwlksn  27818  clwwlkinwwlk  27820  wwlksext2clwwlk  27838  3vfriswmgr  28059  homco1  29580  homulass  29581  hoadddir  29583  satffunlem  32650  mblfinlem3  34933  zerdivemp1x  35227  athgt  36594  psubspi  36885  paddasslem14  36971  eluzge0nn0  43519  iccpartigtl  43590  lighneal  43783  isomgrsym  44008