Theorem 3imp2 1351

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  wereu  5628  dff14i  7215  ovg  7533  fisup2g  9384  fiinf2g  9417  cfcoflem  10194  ttukeylem5  10435  dedekindle  11309  grplcan  18942  mulgnnass  19051  dmdprdsplit2  19989  mulgass2  20256  lmodvsdi  20848  lmodvsdir  20849  lmodvsass  20850  lss1d  20926  islmhm2  21002  lspsolvlem  21109  lbsextlem2  21126  cygznlem2a  21534  isphld  21621  t0dist  23281  hausnei  23284  nrmsep3  23311  fclsopni  23971  fcfneii  23993  ax5seglem5  29018  axcont  29061  grporcan  30605  grpolcan  30617  slmdvsdi  33308  slmdvsdir  33309  slmdvsass  33310  elrspunidl  33520  zarcmplem  34058  mclsppslem  35796  broutsideof2  36335  poimirlem31  37899  broucube  37902  frinfm  37983  crngm23  38250  pridl  38285  pridlc  38319  dmnnzd  38323  dmncan1  38324  paddasslem5  40197  or2expropbi  47391  elsetpreimafveqfv  47749  sfprmdvdsmersenne  47960  isgrtri  48300  grlimprclnbgr  48353