Theorem 3imp2 1368

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  wereu  5647  dff14i  7261  ovg  7583  fisup2g  9454  fiinf2g  9487  cfcoflem  10343  ttukeylem5  10584  dedekindle  11467  grplcan  19204  mulgnnass  19312  dmdprdsplit2  20255  mulgass2  20533  lmodvsdi  21153  lmodvsdir  21154  lmodvsass  21155  lss1d  21231  islmhm2  21306  lspsolvlem  21413  lbsextlem2  21430  unichnlidl  21509  cygznlem2a  21866  isphld  21953  t0dist  23636  hausnei  23639  nrmsep3  23666  fclsopni  24327  fcfneii  24349  ax5seglem5  29504  axcont  29547  grporcan  31113  grpolcan  31125  slmdvsdi  33769  slmdvsdir  33770  slmdvsass  33771  elrspunidl  33971  zarcmplem  34506  mclsppslem  36327  broutsideof2  36867  poimirlem31  38549  broucube  38552  frinfm  38649  crngm23  38916  pridl  38951  pridlc  38985  dmnnzd  38989  dmncan1  38990  paddasslem5  40861  or2expropbi  48073  elsetpreimafveqfv  48443  sfprmdvdsmersenne  48657  isgrtri  49010  grlimprclnbgr  49063  idomnzd  49412  idomcanl  49413