Theorem 3imp2 1349

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

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

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  wereu  5696  ovg  7615  fisup2g  9537  fiinf2g  9569  cfcoflem  10341  ttukeylem5  10582  dedekindle  11454  grplcan  19040  mulgnnass  19149  dmdprdsplit2  20090  mulgass2  20332  lmodvsdi  20905  lmodvsdir  20906  lmodvsass  20907  lss1d  20984  islmhm2  21060  lspsolvlem  21167  lbsextlem2  21184  cygznlem2a  21609  isphld  21695  t0dist  23354  hausnei  23357  nrmsep3  23384  fclsopni  24044  fcfneii  24066  ax5seglem5  28966  axcont  29009  grporcan  30550  grpolcan  30562  slmdvsdi  33194  slmdvsdir  33195  slmdvsass  33196  elrspunidl  33421  zarcmplem  33827  mclsppslem  35551  broutsideof2  36086  poimirlem31  37611  broucube  37614  frinfm  37695  crngm23  37962  pridl  37997  pridlc  38031  dmnnzd  38035  dmncan1  38036  paddasslem5  39781  or2expropbi  46949  elsetpreimafveqfv  47266  sfprmdvdsmersenne  47477  isgrtri  47794