Theorem ancomsd 467

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  sylan2d  606  anabsi6  668  mpand  693  2eu3  2653  ralcom2  3308  somo  5551  wereu2  5597  smoel  8222  cfub  10051  cofsmo  10071  grudomon  10619  axpre-sup  10971  leltadd  11505  lemul12b  11878  lbzbi  12722  injresinj  13554  swrdnnn0nd  14414  abslt  15071  absle  15072  o1lo1  15291  o1co  15340  rlimno1  15410  dvdssub2  16055  lublecllem  18123  f1omvdco2  19101  ptpjpre1  22767  iocopnst  24148  ovolicc2lem4  24729  itg2le  24949  ulmcau  25599  cxpeq0  25878  pntrsumbnd2  26760  cvcon3  30691  atexch  30788  abfmpeld  31036  wsuclem  33864  btwntriv2  34359  btwnexch3  34367  isbasisrelowllem1  35570  isbasisrelowllem2  35571  relowlssretop  35578  finxpsuclem  35612  isinf2  35620  finixpnum  35806  fin2solem  35807  ltflcei  35809  poimirlem27  35848  itg2addnclem  35872  unirep  35915  prter2  36937  cvrcon3b  37333  sn-negex12  40435  fltaccoprm  40514  incssnn0  40570  eldioph4b  40670  fphpdo  40676  pellexlem5  40692  pm14.24  42088  icceuelpart  44946  prsprel  44997  sprsymrelfolem2  45003  goldbachthlem2  45056  gbegt5  45271  aacllem  46563