Theorem 3imp2 1366

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  wereu  5655  dff14i  7255  ovg  7573  fisup2g  9425  fiinf2g  9458  cfcoflem  10252  ttukeylem5  10493  dedekindle  11370  grplcan  19063  mulgnnass  19171  dmdprdsplit2  20114  mulgass2  20388  lmodvsdi  20980  lmodvsdir  20981  lmodvsass  20982  lss1d  21058  islmhm2  21133  lspsolvlem  21240  lbsextlem2  21257  unichnlidl  21336  cygznlem2a  21682  isphld  21769  t0dist  23447  hausnei  23450  nrmsep3  23477  fclsopni  24137  fcfneii  24159  ax5seglem5  29220  axcont  29263  grporcan  30807  grpolcan  30819  slmdvsdi  33472  slmdvsdir  33473  slmdvsass  33474  elrspunidl  33676  zarcmplem  34212  mclsppslem  35970  broutsideof2  36509  poimirlem31  38185  broucube  38188  frinfm  38269  crngm23  38536  pridl  38571  pridlc  38605  dmnnzd  38609  dmncan1  38610  paddasslem5  40483  or2expropbi  47653  elsetpreimafveqfv  48023  sfprmdvdsmersenne  48237  isgrtri  48590  grlimprclnbgr  48643