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  5576  ovg  7415  fisup2g  9157  fiinf2g  9189  cfcoflem  9959  ttukeylem5  10200  dedekindle  11069  grplcan  18552  mulgnnass  18653  dmdprdsplit2  19564  mulgass2  19755  lmodvsdi  20061  lmodvsdir  20062  lmodvsass  20063  lss1d  20140  islmhm2  20215  lspsolvlem  20319  lbsextlem2  20336  cygznlem2a  20687  isphld  20771  t0dist  22384  hausnei  22387  nrmsep3  22414  fclsopni  23074  fcfneii  23096  ax5seglem5  27204  axcont  27247  grporcan  28781  grpolcan  28793  slmdvsdi  31370  slmdvsdir  31371  slmdvsass  31372  elrspunidl  31508  zarcmplem  31733  mclsppslem  33445  broutsideof2  34351  poimirlem31  35735  broucube  35738  frinfm  35820  crngm23  36087  pridl  36122  pridlc  36156  dmnnzd  36160  dmncan1  36161  paddasslem5  37765  or2expropbi  44415  elsetpreimafveqfv  44732  sfprmdvdsmersenne  44943