Theorem ancomsd 468

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  sylan2d  606  anabsi6  668  mpand  693  2eu3  2738  ralcom2  3363  somo  5510  wereu2  5552  smoel  7997  cfub  9671  cofsmo  9691  grudomon  10239  axpre-sup  10591  leltadd  11124  lemul12b  11497  lbzbi  12337  injresinj  13159  swrdnnn0nd  14018  abslt  14674  absle  14675  o1lo1  14894  o1co  14943  rlimno1  15010  dvdssub2  15651  lublecllem  17598  f1omvdco2  18576  ptpjpre1  22179  iocopnst  23544  ovolicc2lem4  24121  itg2le  24340  ulmcau  24983  cxpeq0  25261  pntrsumbnd2  26143  cvcon3  30061  atexch  30158  abfmpeld  30399  wsuclem  33112  btwntriv2  33473  btwnexch3  33481  isbasisrelowllem1  34639  isbasisrelowllem2  34640  relowlssretop  34647  finxpsuclem  34681  isinf2  34689  finixpnum  34892  fin2solem  34893  ltflcei  34895  poimirlem27  34934  itg2addnclem  34958  unirep  35003  prter2  36032  cvrcon3b  36428  incssnn0  39328  eldioph4b  39428  fphpdo  39434  pellexlem5  39450  pm14.24  40784  icceuelpart  43616  prsprel  43669  sprsymrelfolem2  43675  goldbachthlem2  43728  gbegt5  43946  aacllem  44922