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  2648  ralcom2  3353  somo  5588  wereu2  5638  smoel  8332  cfub  10209  cofsmo  10229  grudomon  10777  axpre-sup  11129  leltadd  11669  lemul12b  12046  lbzbi  12902  injresinj  13756  swrdnnn0nd  14628  abslt  15288  absle  15289  o1lo1  15510  o1co  15559  rlimno1  15627  dvdssub2  16278  lublecllem  18326  f1omvdco2  19385  ptpjpre1  23465  iocopnst  24844  ovolicc2lem4  25428  itg2le  25647  ulmcau  26311  cxpeq0  26594  pntrsumbnd2  27485  absslt  28158  cvcon3  32220  atexch  32317  abfmpeld  32585  wsuclem  35820  btwntriv2  36007  btwnexch3  36015  isbasisrelowllem1  37350  isbasisrelowllem2  37351  relowlssretop  37358  finxpsuclem  37392  isinf2  37400  finixpnum  37606  fin2solem  37607  ltflcei  37609  poimirlem27  37648  itg2addnclem  37672  unirep  37715  prter2  38881  cvrcon3b  39277  fltaccoprm  42635  incssnn0  42706  eldioph4b  42806  fphpdo  42812  pellexlem5  42828  pm14.24  44428  traxext  44974  icceuelpart  47441  prsprel  47492  sprsymrelfolem2  47498  goldbachthlem2  47551  gbegt5  47766  aacllem  49794