Theorem 3imp2 1348

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 1347	. 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  5684  ovg  7597  fisup2g  9505  fiinf2g  9537  cfcoflem  10309  ttukeylem5  10550  dedekindle  11422  grplcan  19030  mulgnnass  19139  dmdprdsplit2  20080  mulgass2  20322  lmodvsdi  20899  lmodvsdir  20900  lmodvsass  20901  lss1d  20978  islmhm2  21054  lspsolvlem  21161  lbsextlem2  21178  cygznlem2a  21603  isphld  21689  t0dist  23348  hausnei  23351  nrmsep3  23378  fclsopni  24038  fcfneii  24060  ax5seglem5  28962  axcont  29005  grporcan  30546  grpolcan  30558  slmdvsdi  33203  slmdvsdir  33204  slmdvsass  33205  elrspunidl  33435  zarcmplem  33841  mclsppslem  35567  broutsideof2  36103  poimirlem31  37637  broucube  37640  frinfm  37721  crngm23  37988  pridl  38023  pridlc  38057  dmnnzd  38061  dmncan1  38062  paddasslem5  39806  or2expropbi  46983  elsetpreimafveqfv  47316  sfprmdvdsmersenne  47527  isgrtri  47847