Theorem ancomsd 465

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 416	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
3	2	impd 410	1 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 395

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

This theorem is referenced by:  sylan2d  605  anabsi6  670  mpand  695  2eu3  2653  ralcom2  3356  somo  5600  wereu2  5651  smoel  8374  cfub  10263  cofsmo  10283  grudomon  10831  axpre-sup  11183  leltadd  11721  lemul12b  12098  lbzbi  12952  injresinj  13804  swrdnnn0nd  14674  abslt  15333  absle  15334  o1lo1  15553  o1co  15602  rlimno1  15670  dvdssub2  16320  lublecllem  18370  f1omvdco2  19429  ptpjpre1  23509  iocopnst  24888  ovolicc2lem4  25473  itg2le  25692  ulmcau  26356  cxpeq0  26639  pntrsumbnd2  27530  absslt  28203  cvcon3  32265  atexch  32362  abfmpeld  32632  wsuclem  35843  btwntriv2  36030  btwnexch3  36038  isbasisrelowllem1  37373  isbasisrelowllem2  37374  relowlssretop  37381  finxpsuclem  37415  isinf2  37423  finixpnum  37629  fin2solem  37630  ltflcei  37632  poimirlem27  37671  itg2addnclem  37695  unirep  37738  prter2  38899  cvrcon3b  39295  fltaccoprm  42663  incssnn0  42734  eldioph4b  42834  fphpdo  42840  pellexlem5  42856  pm14.24  44456  traxext  45002  icceuelpart  47450  prsprel  47501  sprsymrelfolem2  47507  goldbachthlem2  47560  gbegt5  47775  aacllem  49665