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  5620  dff14i  7205  ovg  7523  fisup2g  9372  fiinf2g  9405  cfcoflem  10182  ttukeylem5  10423  dedekindle  11297  grplcan  18930  mulgnnass  19039  dmdprdsplit2  19977  mulgass2  20244  lmodvsdi  20836  lmodvsdir  20837  lmodvsass  20838  lss1d  20914  islmhm2  20990  lspsolvlem  21097  lbsextlem2  21114  cygznlem2a  21522  isphld  21609  t0dist  23269  hausnei  23272  nrmsep3  23299  fclsopni  23959  fcfneii  23981  ax5seglem5  29006  axcont  29049  grporcan  30593  grpolcan  30605  slmdvsdi  33297  slmdvsdir  33298  slmdvsass  33299  elrspunidl  33509  zarcmplem  34038  mclsppslem  35777  broutsideof2  36316  poimirlem31  37852  broucube  37855  frinfm  37936  crngm23  38203  pridl  38238  pridlc  38272  dmnnzd  38276  dmncan1  38277  paddasslem5  40084  or2expropbi  47280  elsetpreimafveqfv  47638  sfprmdvdsmersenne  47849  isgrtri  48189  grlimprclnbgr  48242