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  606  anabsi6  671  mpand  696  2eu3  2655  ralcom2  3349  somo  5579  wereu2  5629  smoel  8302  cfub  10171  cofsmo  10191  grudomon  10740  axpre-sup  11092  leltadd  11633  lemul12b  12010  lbzbi  12861  injresinj  13719  swrdnnn0nd  14592  abslt  15250  absle  15251  o1lo1  15472  o1co  15521  rlimno1  15589  dvdssub2  16240  lublecllem  18293  f1omvdco2  19389  ptpjpre1  23527  iocopnst  24905  ovolicc2lem4  25489  itg2le  25708  ulmcau  26372  cxpeq0  26655  pntrsumbnd2  27546  abslts  28257  cvcon3  32371  atexch  32468  abfmpeld  32743  r1filimi  35278  noinfepfnregs  35307  wsuclem  36036  btwntriv2  36225  btwnexch3  36233  isbasisrelowllem1  37599  isbasisrelowllem2  37600  relowlssretop  37607  finxpsuclem  37641  isinf2  37649  finixpnum  37845  fin2solem  37846  ltflcei  37848  poimirlem27  37887  itg2addnclem  37911  unirep  37954  prter2  39246  cvrcon3b  39642  fltaccoprm  42987  incssnn0  43057  eldioph4b  43157  fphpdo  43163  pellexlem5  43179  pm14.24  44777  traxext  45322  icceuelpart  47785  prsprel  47836  sprsymrelfolem2  47842  goldbachthlem2  47895  gbegt5  48110  aacllem  50149