Theorem 3imp1 1344

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  3an1rs  1356  reupick2  4241  indcardi  9452  ledivge1le  12448  expcan  13529  ltexp2  13530  leexp1a  13535  expnbnd  13589  cshf1  14163  rtrclreclem4  14412  relexpindlem  14414  ncoprmlnprm  16058  xrsdsreclblem  20137  matecl  21030  scmateALT  21117  riinopn  21513  neindisj2  21728  filufint  22525  tsmsxp  22760  ewlkle  27395  uspgr2wlkeq  27435  spthonepeq  27541  wwlksm1edg  27667  clwwisshclwws  27800  clwwlknwwlksn  27823  clwwlkinwwlk  27825  wwlksext2clwwlk  27842  3vfriswmgr  28063  homco1  29584  homulass  29585  hoadddir  29587  satffunlem  32761  mblfinlem3  35096  zerdivemp1x  35385  athgt  36752  psubspi  37043  paddasslem14  37129  eluzge0nn0  43869  iccpartigtl  43940  lighneal  44129  isomgrsym  44354