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  5619  dff14i  7200  ovg  7518  fisup2g  9378  fiinf2g  9411  cfcoflem  10185  ttukeylem5  10426  dedekindle  11298  grplcan  18897  mulgnnass  19006  dmdprdsplit2  19945  mulgass2  20212  lmodvsdi  20806  lmodvsdir  20807  lmodvsass  20808  lss1d  20884  islmhm2  20960  lspsolvlem  21067  lbsextlem2  21084  cygznlem2a  21492  isphld  21579  t0dist  23228  hausnei  23231  nrmsep3  23258  fclsopni  23918  fcfneii  23940  ax5seglem5  28896  axcont  28939  grporcan  30480  grpolcan  30492  slmdvsdi  33170  slmdvsdir  33171  slmdvsass  33172  elrspunidl  33378  zarcmplem  33850  mclsppslem  35558  broutsideof2  36098  poimirlem31  37633  broucube  37636  frinfm  37717  crngm23  37984  pridl  38019  pridlc  38053  dmnnzd  38057  dmncan1  38058  paddasslem5  39806  or2expropbi  47022  elsetpreimafveqfv  47380  sfprmdvdsmersenne  47591  isgrtri  47931  grlimprclnbgr  47984