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  5637  dff14i  7237  ovg  7557  fisup2g  9427  fiinf2g  9460  cfcoflem  10232  ttukeylem5  10473  dedekindle  11345  grplcan  18939  mulgnnass  19048  dmdprdsplit2  19985  mulgass2  20225  lmodvsdi  20798  lmodvsdir  20799  lmodvsass  20800  lss1d  20876  islmhm2  20952  lspsolvlem  21059  lbsextlem2  21076  cygznlem2a  21484  isphld  21570  t0dist  23219  hausnei  23222  nrmsep3  23249  fclsopni  23909  fcfneii  23931  ax5seglem5  28867  axcont  28910  grporcan  30454  grpolcan  30466  slmdvsdi  33175  slmdvsdir  33176  slmdvsass  33177  elrspunidl  33406  zarcmplem  33878  mclsppslem  35577  broutsideof2  36117  poimirlem31  37652  broucube  37655  frinfm  37736  crngm23  38003  pridl  38038  pridlc  38072  dmnnzd  38076  dmncan1  38077  paddasslem5  39825  or2expropbi  47039  elsetpreimafveqfv  47397  sfprmdvdsmersenne  47608  isgrtri  47946