Theorem 3imp2 1348

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  wereu  5617  ovg  7500  fisup2g  9326  fiinf2g  9358  cfcoflem  10130  ttukeylem5  10371  dedekindle  11241  grplcan  18734  mulgnnass  18835  dmdprdsplit2  19745  mulgass2  19936  lmodvsdi  20253  lmodvsdir  20254  lmodvsass  20255  lss1d  20332  islmhm2  20407  lspsolvlem  20511  lbsextlem2  20528  cygznlem2a  20882  isphld  20966  t0dist  22583  hausnei  22586  nrmsep3  22613  fclsopni  23273  fcfneii  23295  ax5seglem5  27591  axcont  27634  grporcan  29169  grpolcan  29181  slmdvsdi  31755  slmdvsdir  31756  slmdvsass  31757  elrspunidl  31903  zarcmplem  32129  mclsppslem  33844  broutsideof2  34563  poimirlem31  35964  broucube  35967  frinfm  36049  crngm23  36316  pridl  36351  pridlc  36385  dmnnzd  36389  dmncan1  36390  paddasslem5  38143  or2expropbi  44946  elsetpreimafveqfv  45262  sfprmdvdsmersenne  45473