Theorem 3imp2 1345

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  wereu  5545  ovg  7307  fisup2g  8926  fiinf2g  8958  cfcoflem  9688  ttukeylem5  9929  dedekindle  10798  grplcan  18155  mulgnnass  18256  dmdprdsplit2  19162  mulgass2  19345  lmodvsdi  19651  lmodvsdir  19652  lmodvsass  19653  lss1d  19729  islmhm2  19804  lspsolvlem  19908  lbsextlem2  19925  cygznlem2a  20708  isphld  20792  t0dist  21927  hausnei  21930  nrmsep3  21957  fclsopni  22617  fcfneii  22639  ax5seglem5  26713  axcont  26756  grporcan  28289  grpolcan  28301  slmdvsdi  30838  slmdvsdir  30839  slmdvsass  30840  mclsppslem  32825  broutsideof2  33578  poimirlem31  34917  broucube  34920  frinfm  35004  crngm23  35274  pridl  35309  pridlc  35343  dmnnzd  35347  dmncan1  35348  paddasslem5  36954  or2expropbi  43263  elsetpreimafveqfv  43546  sfprmdvdsmersenne  43762