Theorem 3imp2 1350

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 1349	. 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  5681  ovg  7598  fisup2g  9508  fiinf2g  9540  cfcoflem  10312  ttukeylem5  10553  dedekindle  11425  grplcan  19018  mulgnnass  19127  dmdprdsplit2  20066  mulgass2  20306  lmodvsdi  20883  lmodvsdir  20884  lmodvsass  20885  lss1d  20961  islmhm2  21037  lspsolvlem  21144  lbsextlem2  21161  cygznlem2a  21586  isphld  21672  t0dist  23333  hausnei  23336  nrmsep3  23363  fclsopni  24023  fcfneii  24045  ax5seglem5  28948  axcont  28991  grporcan  30537  grpolcan  30549  slmdvsdi  33221  slmdvsdir  33222  slmdvsass  33223  elrspunidl  33456  zarcmplem  33880  mclsppslem  35588  broutsideof2  36123  poimirlem31  37658  broucube  37661  frinfm  37742  crngm23  38009  pridl  38044  pridlc  38078  dmnnzd  38082  dmncan1  38083  paddasslem5  39826  or2expropbi  47046  elsetpreimafveqfv  47379  sfprmdvdsmersenne  47590  isgrtri  47910