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  3341  somo  5561  wereu2  5611  smoel  8275  cfub  10132  cofsmo  10152  grudomon  10700  axpre-sup  11052  leltadd  11593  lemul12b  11970  lbzbi  12826  injresinj  13683  swrdnnn0nd  14556  abslt  15214  absle  15215  o1lo1  15436  o1co  15485  rlimno1  15553  dvdssub2  16204  lublecllem  18256  f1omvdco2  19353  ptpjpre1  23479  iocopnst  24857  ovolicc2lem4  25441  itg2le  25660  ulmcau  26324  cxpeq0  26607  pntrsumbnd2  27498  absslt  28180  cvcon3  32254  atexch  32351  abfmpeld  32626  wsuclem  35838  btwntriv2  36025  btwnexch3  36033  isbasisrelowllem1  37368  isbasisrelowllem2  37369  relowlssretop  37376  finxpsuclem  37410  isinf2  37418  finixpnum  37624  fin2solem  37625  ltflcei  37627  poimirlem27  37666  itg2addnclem  37690  unirep  37733  prter2  38899  cvrcon3b  39295  fltaccoprm  42652  incssnn0  42723  eldioph4b  42823  fphpdo  42829  pellexlem5  42845  pm14.24  44444  traxext  44989  icceuelpart  47446  prsprel  47497  sprsymrelfolem2  47503  goldbachthlem2  47556  gbegt5  47771  aacllem  49812