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 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  wereu  5610  dff14i  7193  ovg  7511  fisup2g  9353  fiinf2g  9386  cfcoflem  10163  ttukeylem5  10404  dedekindle  11277  grplcan  18913  mulgnnass  19022  dmdprdsplit2  19960  mulgass2  20227  lmodvsdi  20818  lmodvsdir  20819  lmodvsass  20820  lss1d  20896  islmhm2  20972  lspsolvlem  21079  lbsextlem2  21096  cygznlem2a  21504  isphld  21591  t0dist  23240  hausnei  23243  nrmsep3  23270  fclsopni  23930  fcfneii  23952  ax5seglem5  28911  axcont  28954  grporcan  30498  grpolcan  30510  slmdvsdi  33184  slmdvsdir  33185  slmdvsass  33186  elrspunidl  33393  zarcmplem  33894  mclsppslem  35627  broutsideof2  36166  poimirlem31  37690  broucube  37693  frinfm  37774  crngm23  38041  pridl  38076  pridlc  38110  dmnnzd  38114  dmncan1  38115  paddasslem5  39922  or2expropbi  47133  elsetpreimafveqfv  47491  sfprmdvdsmersenne  47702  isgrtri  48042  grlimprclnbgr  48095