Theorem ancomsd 469

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  sylan2d  607  anabsi6  669  mpand  694  2eu3  2675  ralcom2  3282  somo  5484  wereu2  5526  smoel  8014  cfub  9723  cofsmo  9743  grudomon  10291  axpre-sup  10643  leltadd  11176  lemul12b  11549  lbzbi  12390  injresinj  13221  swrdnnn0nd  14079  abslt  14736  absle  14737  o1lo1  14956  o1co  15005  rlimno1  15072  dvdssub2  15716  lublecllem  17679  f1omvdco2  18658  ptpjpre1  22286  iocopnst  23656  ovolicc2lem4  24235  itg2le  24454  ulmcau  25104  cxpeq0  25383  pntrsumbnd2  26265  cvcon3  30181  atexch  30278  abfmpeld  30529  wsuclem  33388  btwntriv2  33899  btwnexch3  33907  isbasisrelowllem1  35088  isbasisrelowllem2  35089  relowlssretop  35096  finxpsuclem  35130  isinf2  35138  finixpnum  35358  fin2solem  35359  ltflcei  35361  poimirlem27  35400  itg2addnclem  35424  unirep  35467  prter2  36493  cvrcon3b  36889  sn-negex12  39941  fltaccoprm  40015  incssnn0  40071  eldioph4b  40171  fphpdo  40177  pellexlem5  40193  pm14.24  41555  icceuelpart  44381  prsprel  44432  sprsymrelfolem2  44438  goldbachthlem2  44491  gbegt5  44706  aacllem  45827