Theorem 3imp2 1351

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 1350	. 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  5620  dff14i  7207  ovg  7525  fisup2g  9375  fiinf2g  9408  cfcoflem  10185  ttukeylem5  10426  dedekindle  11301  grplcan  18967  mulgnnass  19076  dmdprdsplit2  20014  mulgass2  20281  lmodvsdi  20871  lmodvsdir  20872  lmodvsass  20873  lss1d  20949  islmhm2  21025  lspsolvlem  21132  lbsextlem2  21149  cygznlem2a  21557  isphld  21644  t0dist  23300  hausnei  23303  nrmsep3  23330  fclsopni  23990  fcfneii  24012  ax5seglem5  29016  axcont  29059  grporcan  30604  grpolcan  30616  slmdvsdi  33291  slmdvsdir  33292  slmdvsass  33293  elrspunidl  33503  zarcmplem  34041  mclsppslem  35781  broutsideof2  36320  poimirlem31  37986  broucube  37989  frinfm  38070  crngm23  38337  pridl  38372  pridlc  38406  dmnnzd  38410  dmncan1  38411  paddasslem5  40284  or2expropbi  47494  elsetpreimafveqfv  47864  sfprmdvdsmersenne  48078  isgrtri  48431  grlimprclnbgr  48484