Theorem ancomsd 470

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  sylan2d  616  anabsi6  682  mpand  707  2eu3  2679  ralcom2  3364  somo  5608  wereu2  5658  smoel  8346  cfub  10231  cofsmo  10252  grudomon  10801  axpre-sup  11153  leltadd  11697  lemul12b  12071  lbzbi  12959  injresinj  13820  swrdnnn0nd  14694  abslt  15366  absle  15367  o1lo1  15588  o1co  15637  rlimno1  15705  dvdssub2  16358  lublecllem  18413  f1omvdco2  19517  ptpjpre1  23707  iocopnst  25078  ovolicc2lem4  25658  itg2le  25877  ulmcau  26534  cxpeq0  26819  pntrsumbnd2  27707  abslts  28418  cvcon3  32602  atexch  32699  abfmpeld  32965  r1filimi  35463  noinfepfnregs  35511  wsuclem  36281  btwntriv2  36470  btwnexch3  36478  isbasisrelowllem1  37967  isbasisrelowllem2  37968  relowlssretop  37975  finxpsuclem  38009  isinf2  38017  finixpnum  38222  fin2solem  38223  ltflcei  38225  poimirlem27  38264  itg2addnclem  38288  unirep  38331  prter2  39623  cvrcon3b  40019  fltaccoprm  43342  incssnn0  43412  eldioph4b  43508  fphpdo  43514  pellexlem5  43530  pm14.24  45112  traxext  45656  icceuelpart  48152  prsprel  48203  sprsymrelfolem2  48209  goldbachthlem2  48265  gbegt5  48493  aacllem  50568