Theorem ancomsd 466

Description: Deduction commuting conjunction in antecedent. (Contributed by NM, 12-Dec-2004.)

Hypothesis

Ref	Expression
ancomsd.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
ancomsd	⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))

Proof of Theorem ancomsd

Step	Hyp	Ref	Expression
1		ancomsd.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expcomd 417	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
3	2	impd 411	1 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 396

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

This theorem is referenced by:  sylan2d  604  anabsi6  666  mpand  691  2eu3  2711  ralcom2  3326  somo  5405  wereu2  5447  smoel  7856  cfub  9524  cofsmo  9544  grudomon  10092  axpre-sup  10444  leltadd  10978  lemul12b  11351  lbzbi  12189  injresinj  13012  swrdnnn0nd  13858  abslt  14512  absle  14513  o1lo1  14732  o1co  14781  rlimno1  14848  dvdssub2  15488  lublecllem  17431  f1omvdco2  18311  ptpjpre1  21867  iocopnst  23231  ovolicc2lem4  23808  itg2le  24027  ulmcau  24670  cxpeq0  24946  pntrsumbnd2  25829  cvcon3  29748  atexch  29845  abfmpeld  30085  wsuclem  32723  btwntriv2  33084  btwnexch3  33092  isbasisrelowllem1  34188  isbasisrelowllem2  34189  relowlssretop  34196  finxpsuclem  34230  isinf2  34238  finixpnum  34429  fin2solem  34430  ltflcei  34432  poimirlem27  34471  itg2addnclem  34495  unirep  34541  prter2  35569  cvrcon3b  35965  incssnn0  38814  eldioph4b  38914  fphpdo  38920  pellexlem5  38936  pm14.24  40323  icceuelpart  43100  prsprel  43153  sprsymrelfolem2  43159  goldbachthlem2  43212  gbegt5  43430  aacllem  44404