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  5651  dff14i  7256  ovg  7578  fisup2g  9439  fiinf2g  9472  cfcoflem  10274  ttukeylem5  10515  dedekindle  11398  grplcan  19124  mulgnnass  19232  dmdprdsplit2  20175  mulgass2  20451  lmodvsdi  21069  lmodvsdir  21070  lmodvsass  21071  lss1d  21147  islmhm2  21222  lspsolvlem  21329  lbsextlem2  21346  unichnlidl  21425  cygznlem2a  21780  isphld  21867  t0dist  23550  hausnei  23553  nrmsep3  23580  fclsopni  24241  fcfneii  24263  ax5seglem5  29390  axcont  29433  grporcan  30999  grpolcan  31011  slmdvsdi  33655  slmdvsdir  33656  slmdvsass  33657  elrspunidl  33856  zarcmplem  34391  mclsppslem  36162  broutsideof2  36702  poimirlem31  38400  broucube  38403  frinfm  38485  crngm23  38752  pridl  38787  pridlc  38821  dmnnzd  38825  dmncan1  38826  paddasslem5  40697  or2expropbi  47922  elsetpreimafveqfv  48292  sfprmdvdsmersenne  48506  isgrtri  48859  grlimprclnbgr  48912  idomnzd  49261  idomcanl  49262