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  5634  dff14i  7234  ovg  7554  fisup2g  9420  fiinf2g  9453  cfcoflem  10225  ttukeylem5  10466  dedekindle  11338  grplcan  18932  mulgnnass  19041  dmdprdsplit2  19978  mulgass2  20218  lmodvsdi  20791  lmodvsdir  20792  lmodvsass  20793  lss1d  20869  islmhm2  20945  lspsolvlem  21052  lbsextlem2  21069  cygznlem2a  21477  isphld  21563  t0dist  23212  hausnei  23215  nrmsep3  23242  fclsopni  23902  fcfneii  23924  ax5seglem5  28860  axcont  28903  grporcan  30447  grpolcan  30459  slmdvsdi  33168  slmdvsdir  33169  slmdvsass  33170  elrspunidl  33399  zarcmplem  33871  mclsppslem  35570  broutsideof2  36110  poimirlem31  37645  broucube  37648  frinfm  37729  crngm23  37996  pridl  38031  pridlc  38065  dmnnzd  38069  dmncan1  38070  paddasslem5  39818  or2expropbi  47035  elsetpreimafveqfv  47393  sfprmdvdsmersenne  47604  isgrtri  47942