Theorem 3imp2 1443

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  wereu  5262  ovg  6964  fisup2g  8539  fiinf2g  8571  cfcoflem  9286  ttukeylem5  9527  dedekindle  10393  grplcan  17678  mulgnnass  17777  mulgnnassOLD  17778  dmdprdsplit2  18645  mulgass2  18801  lmodvsdi  19088  lmodvsdir  19089  lmodvsass  19090  lss1d  19165  islmhm2  19240  lspsolvlem  19344  lbsextlem2  19361  cygznlem2a  20118  isphld  20201  t0dist  21331  hausnei  21334  nrmsep3  21361  fclsopni  22020  fcfneii  22042  ax5seglem5  26012  axcont  26055  grporcan  27681  grpolcan  27693  slmdvsdi  30077  slmdvsdir  30078  slmdvsass  30079  mclsppslem  31787  broutsideof2  32535  poimirlem31  33753  broucube  33756  frinfm  33843  crngm23  34114  pridl  34149  pridlc  34183  dmnnzd  34187  dmncan1  34188  paddasslem5  35613  sfprmdvdsmersenne  42030