Theorem 3imp2 1342

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  wereu  5446  ovg  7176  fisup2g  8785  fiinf2g  8817  cfcoflem  9547  ttukeylem5  9788  dedekindle  10657  grplcan  17922  mulgnnass  18020  dmdprdsplit2  18889  mulgass2  19045  lmodvsdi  19351  lmodvsdir  19352  lmodvsass  19353  lss1d  19429  islmhm2  19504  lspsolvlem  19608  lbsextlem2  19625  cygznlem2a  20400  isphld  20484  t0dist  21621  hausnei  21624  nrmsep3  21651  fclsopni  22311  fcfneii  22333  ax5seglem5  26406  axcont  26449  grporcan  27982  grpolcan  27994  slmdvsdi  30477  slmdvsdir  30478  slmdvsass  30479  mclsppslem  32440  broutsideof2  33194  poimirlem31  34475  broucube  34478  frinfm  34563  crngm23  34833  pridl  34868  pridlc  34902  dmnnzd  34906  dmncan1  34907  paddasslem5  36512  or2expropbi  42807  sfprmdvdsmersenne  43272