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  2647  ralcom2  3351  somo  5585  wereu2  5635  smoel  8329  cfub  10202  cofsmo  10222  grudomon  10770  axpre-sup  11122  leltadd  11662  lemul12b  12039  lbzbi  12895  injresinj  13749  swrdnnn0nd  14621  abslt  15281  absle  15282  o1lo1  15503  o1co  15552  rlimno1  15620  dvdssub2  16271  lublecllem  18319  f1omvdco2  19378  ptpjpre1  23458  iocopnst  24837  ovolicc2lem4  25421  itg2le  25640  ulmcau  26304  cxpeq0  26587  pntrsumbnd2  27478  absslt  28151  cvcon3  32213  atexch  32310  abfmpeld  32578  wsuclem  35813  btwntriv2  36000  btwnexch3  36008  isbasisrelowllem1  37343  isbasisrelowllem2  37344  relowlssretop  37351  finxpsuclem  37385  isinf2  37393  finixpnum  37599  fin2solem  37600  ltflcei  37602  poimirlem27  37641  itg2addnclem  37665  unirep  37708  prter2  38874  cvrcon3b  39270  fltaccoprm  42628  incssnn0  42699  eldioph4b  42799  fphpdo  42805  pellexlem5  42821  pm14.24  44421  traxext  44967  icceuelpart  47437  prsprel  47488  sprsymrelfolem2  47494  goldbachthlem2  47547  gbegt5  47762  aacllem  49790