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 411	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  wereu  5659  dff14i  7259  ovg  7577  fisup2g  9430  fiinf2g  9463  cfcoflem  10257  ttukeylem5  10498  dedekindle  11375  grplcan  19068  mulgnnass  19176  dmdprdsplit2  20119  mulgass2  20393  lmodvsdi  20987  lmodvsdir  20988  lmodvsass  20989  lss1d  21065  islmhm2  21140  lspsolvlem  21247  lbsextlem2  21264  unichnlidl  21343  cygznlem2a  21698  isphld  21785  t0dist  23463  hausnei  23466  nrmsep3  23493  fclsopni  24153  fcfneii  24175  ax5seglem5  29264  axcont  29307  grporcan  30851  grpolcan  30863  slmdvsdi  33516  slmdvsdir  33517  slmdvsass  33518  elrspunidl  33717  zarcmplem  34252  mclsppslem  36056  broutsideof2  36595  poimirlem31  38283  broucube  38286  frinfm  38367  crngm23  38634  pridl  38669  pridlc  38703  dmnnzd  38707  dmncan1  38708  paddasslem5  40579  or2expropbi  47754  elsetpreimafveqfv  48124  sfprmdvdsmersenne  48338  isgrtri  48691  grlimprclnbgr  48744  idomnzd  49094  idomcanl  49095