Theorem 3imp2 1362

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  wereu  5639  dff14i  7238  ovg  7556  fisup2g  9409  fiinf2g  9442  cfcoflem  10223  ttukeylem5  10464  dedekindle  11341  grplcan  19033  mulgnnass  19142  dmdprdsplit2  20079  mulgass2  20346  lmodvsdi  20940  lmodvsdir  20941  lmodvsass  20942  lss1d  21018  islmhm2  21093  lspsolvlem  21200  lbsextlem2  21217  cygznlem2a  21607  isphld  21694  t0dist  23373  hausnei  23376  nrmsep3  23403  fclsopni  24063  fcfneii  24085  ax5seglem5  29091  axcont  29134  grporcan  30678  grpolcan  30690  slmdvsdi  33356  slmdvsdir  33357  slmdvsass  33358  elrspunidl  33575  zarcmplem  34139  mclsppslem  35894  broutsideof2  36433  poimirlem31  38111  broucube  38114  frinfm  38195  crngm23  38462  pridl  38497  pridlc  38531  dmnnzd  38535  dmncan1  38536  paddasslem5  40409  or2expropbi  47589  elsetpreimafveqfv  47959  sfprmdvdsmersenne  48173  isgrtri  48526  grlimprclnbgr  48579