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 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  sylan2d  616  anabsi6  682  mpand  707  2eu3  2680  ralcom2  3365  somo  5607  wereu2  5657  smoel  8345  cfub  10238  cofsmo  10259  grudomon  10808  axpre-sup  11160  leltadd  11704  lemul12b  12078  lbzbi  12966  injresinj  13827  swrdnnn0nd  14701  abslt  15373  absle  15374  o1lo1  15595  o1co  15644  rlimno1  15712  dvdssub2  16365  lublecllem  18420  f1omvdco2  19524  ptpjpre1  23739  iocopnst  25110  ovolicc2lem4  25690  itg2le  25909  ulmcau  26569  cxpeq0  26854  pntrsumbnd2  27742  abslts  28453  cvcon3  32647  atexch  32744  abfmpeld  33010  r1filimi  35506  noinfepfnregs  35553  wsuclem  36323  btwntriv2  36512  btwnexch3  36520  isbasisrelowllem1  38029  isbasisrelowllem2  38030  relowlssretop  38037  finxpsuclem  38071  isinf2  38079  finixpnum  38284  fin2solem  38285  ltflcei  38287  poimirlem27  38326  itg2addnclem  38350  unirep  38393  prter2  39683  cvrcon3b  40079  fltaccoprm  43400  incssnn0  43470  eldioph4b  43566  fphpdo  43572  pellexlem5  43588  pm14.24  45170  traxext  45714  icceuelpart  48213  prsprel  48264  sprsymrelfolem2  48270  goldbachthlem2  48326  gbegt5  48554  aacllem  50649