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  5659  dff14i  7259  ovg  7581  fisup2g  9432  fiinf2g  9465  cfcoflem  10267  ttukeylem5  10508  dedekindle  11385  grplcan  19090  mulgnnass  19198  dmdprdsplit2  20141  mulgass2  20417  lmodvsdi  21035  lmodvsdir  21036  lmodvsass  21037  lss1d  21113  islmhm2  21188  lspsolvlem  21295  lbsextlem2  21312  unichnlidl  21391  cygznlem2a  21746  isphld  21833  t0dist  23511  hausnei  23514  nrmsep3  23541  fclsopni  24201  fcfneii  24223  ax5seglem5  29312  axcont  29355  grporcan  30899  grpolcan  30911  slmdvsdi  33558  slmdvsdir  33559  slmdvsass  33560  elrspunidl  33759  zarcmplem  34294  mclsppslem  36088  broutsideof2  36627  poimirlem31  38335  broucube  38338  frinfm  38419  crngm23  38686  pridl  38721  pridlc  38755  dmnnzd  38759  dmncan1  38760  paddasslem5  40631  or2expropbi  47804  elsetpreimafveqfv  48174  sfprmdvdsmersenne  48388  isgrtri  48741  grlimprclnbgr  48794  idomnzd  49144  idomcanl  49145