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  5652  frinf  6314  dff14i  7292  ovg  7615  fisup2g  9496  fiinf2g  9529  cfcoflem  10387  ttukeylem5  10628  dedekindle  11511  grplcan  19252  mulgnnass  19360  dmdprdsplit2  20304  mulgass2  20582  lmodvsdi  21202  lmodvsdir  21203  lmodvsass  21204  lss1d  21280  islmhm2  21355  lspsolvlem  21462  lbsextlem2  21479  unichnlidl  21558  cygznlem2a  21917  isphld  22004  t0dist  23687  hausnei  23690  nrmsep3  23717  fclsopni  24378  fcfneii  24400  ax5seglem5  29557  axcont  29600  grporcan  31166  grpolcan  31178  slmdvsdi  33865  slmdvsdir  33866  slmdvsass  33867  zarcmplem  34617  mclsppslem  36549  broutsideof2  37095  poimirlem31  38830  broucube  38833  crngm23  39195  pridl  39230  pridlc  39264  dmnnzd  39268  dmncan1  39269  paddasslem5  41140  or2expropbi  48371  elsetpreimafveqfv  48741  sfprmdvdsmersenne  48955  isgrtri  49308  grlimprclnbgr  49361  idomnzd  49768  idomcanl  49769