Theorem 3imp2 1350

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  wereu  5673  ovg  7572  fisup2g  9463  fiinf2g  9495  cfcoflem  10267  ttukeylem5  10508  dedekindle  11378  grplcan  18885  mulgnnass  18989  dmdprdsplit2  19916  mulgass2  20121  lmodvsdi  20495  lmodvsdir  20496  lmodvsass  20497  lss1d  20574  islmhm2  20649  lspsolvlem  20755  lbsextlem2  20772  cygznlem2a  21123  isphld  21207  t0dist  22829  hausnei  22832  nrmsep3  22859  fclsopni  23519  fcfneii  23541  ax5seglem5  28191  axcont  28234  grporcan  29771  grpolcan  29783  slmdvsdi  32360  slmdvsdir  32361  slmdvsass  32362  elrspunidl  32546  zarcmplem  32861  mclsppslem  34574  broutsideof2  35094  poimirlem31  36519  broucube  36522  frinfm  36603  crngm23  36870  pridl  36905  pridlc  36939  dmnnzd  36943  dmncan1  36944  paddasslem5  38695  or2expropbi  45744  elsetpreimafveqfv  46060  sfprmdvdsmersenne  46271