Theorem 3imp2 1347

Description: Importation to right triple conjunction. (Contributed by NM, 26-Oct-2006.)

Hypothesis

Ref	Expression
3imp1.1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Assertion

Ref	Expression
3imp2	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)

Proof of Theorem 3imp2

Step	Hyp	Ref	Expression
1		3imp1.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2	1	3impd 1346	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))
3	2	imp 406	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  wereu  5587  ovg  7457  fisup2g  9255  fiinf2g  9287  cfcoflem  10056  ttukeylem5  10297  dedekindle  11167  grplcan  18665  mulgnnass  18766  dmdprdsplit2  19677  mulgass2  19868  lmodvsdi  20174  lmodvsdir  20175  lmodvsass  20176  lss1d  20253  islmhm2  20328  lspsolvlem  20432  lbsextlem2  20449  cygznlem2a  20803  isphld  20887  t0dist  22504  hausnei  22507  nrmsep3  22534  fclsopni  23194  fcfneii  23216  ax5seglem5  27329  axcont  27372  grporcan  28908  grpolcan  28920  slmdvsdi  31496  slmdvsdir  31497  slmdvsass  31498  elrspunidl  31634  zarcmplem  31859  mclsppslem  33573  broutsideof2  34452  poimirlem31  35836  broucube  35839  frinfm  35921  crngm23  36188  pridl  36223  pridlc  36257  dmnnzd  36261  dmncan1  36262  paddasslem5  37864  or2expropbi  44568  elsetpreimafveqfv  44884  sfprmdvdsmersenne  45095