Theorem 3imp2 1368

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  wereu  5646  dff14i  7263  ovg  7585  fisup2g  9461  fiinf2g  9494  cfcoflem  10350  ttukeylem5  10591  dedekindle  11474  grplcan  19211  mulgnnass  19319  dmdprdsplit2  20262  mulgass2  20540  lmodvsdi  21160  lmodvsdir  21161  lmodvsass  21162  lss1d  21238  islmhm2  21313  lspsolvlem  21420  lbsextlem2  21437  unichnlidl  21516  cygznlem2a  21873  isphld  21960  t0dist  23643  hausnei  23646  nrmsep3  23673  fclsopni  24334  fcfneii  24356  ax5seglem5  29511  axcont  29554  grporcan  31120  grpolcan  31132  slmdvsdi  33776  slmdvsdir  33777  slmdvsass  33778  elrspunidl  33978  zarcmplem  34513  mclsppslem  36348  broutsideof2  36887  poimirlem31  38570  broucube  38573  frinfm  38670  crngm23  38937  pridl  38972  pridlc  39006  dmnnzd  39010  dmncan1  39011  paddasslem5  40882  or2expropbi  48104  elsetpreimafveqfv  48474  sfprmdvdsmersenne  48688  isgrtri  49041  grlimprclnbgr  49094  idomnzd  49443  idomcanl  49444