Theorem 3imp2 1282

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  wereu  5110  ovg  6799  fisup2g  8374  fiinf2g  8406  cfcoflem  9094  ttukeylem5  9335  dedekindle  10201  grplcan  17477  mulgnnass  17576  mulgnnassOLD  17577  dmdprdsplit2  18445  mulgass2  18601  lmodvsdi  18886  lmodvsdir  18887  lmodvsass  18888  lss1d  18963  islmhm2  19038  lspsolvlem  19142  lbsextlem2  19159  cygznlem2a  19916  isphld  19999  t0dist  21129  hausnei  21132  nrmsep3  21159  fclsopni  21819  fcfneii  21841  ax5seglem5  25813  axcont  25856  grporcan  27372  grpolcan  27384  slmdvsdi  29768  slmdvsdir  29769  slmdvsass  29770  mclsppslem  31480  broutsideof2  32229  poimirlem31  33440  broucube  33443  frinfm  33530  crngm23  33801  pridl  33836  pridlc  33870  dmnnzd  33874  dmncan1  33875  paddasslem5  35110  sfprmdvdsmersenne  41520