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  5617  dff14i  7201  ovg  7519  fisup2g  9362  fiinf2g  9395  cfcoflem  10172  ttukeylem5  10413  dedekindle  11286  grplcan  18917  mulgnnass  19026  dmdprdsplit2  19964  mulgass2  20231  lmodvsdi  20822  lmodvsdir  20823  lmodvsass  20824  lss1d  20900  islmhm2  20976  lspsolvlem  21083  lbsextlem2  21100  cygznlem2a  21508  isphld  21595  t0dist  23243  hausnei  23246  nrmsep3  23273  fclsopni  23933  fcfneii  23955  ax5seglem5  28915  axcont  28958  grporcan  30502  grpolcan  30514  slmdvsdi  33193  slmdvsdir  33194  slmdvsass  33195  elrspunidl  33402  zarcmplem  33917  mclsppslem  35650  broutsideof2  36189  poimirlem31  37714  broucube  37717  frinfm  37798  crngm23  38065  pridl  38100  pridlc  38134  dmnnzd  38138  dmncan1  38139  paddasslem5  39946  or2expropbi  47161  elsetpreimafveqfv  47519  sfprmdvdsmersenne  47730  isgrtri  48070  grlimprclnbgr  48123