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		ancom 465	. 2 ⊢ ((𝜒 ∧ 𝜓) ↔ (𝜓 ∧ 𝜒))
2		ancomsd.1	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	1, 2	syl5bi 231	1 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  sylan2d  498  mpand  707  anabsi6  855  ralcom2  3083  ralxfrdOLD  4806  somo  4993  wereu2  5035  poirr2  5439  smoel  7344  cfub  8954  cofsmo  8974  grudomon  9518  axpre-sup  9869  leltadd  10391  lemul12b  10759  lbzbi  11652  injresinj  12451  abslt  13902  absle  13903  o1lo1  14116  o1co  14165  rlimno1  14232  znnenlem  14779  dvdssub2  14861  lublecllem  16811  f1omvdco2  17691  ptpjpre1  21184  iocopnst  22547  ovolicc2lem4  23095  itg2le  23312  ulmcau  23953  cxpeq0  24224  pntrsumbnd2  25056  cvcon3  28527  atexch  28624  abfmpeld  28834  wsuclem  31017  wsuclemOLD  31018  nofulllem5  31105  btwntriv2  31289  btwnexch3  31297  isbasisrelowllem1  32379  isbasisrelowllem2  32380  relowlssretop  32387  finxpsuclem  32410  finixpnum  32564  fin2solem  32565  ltflcei  32567  poimirlem27  32606  itg2addnclem  32631  unirep  32677  prter2  33184  cvrcon3b  33582  incssnn0  36292  eldioph4b  36393  fphpdo  36399  pellexlem5  36415  pm14.24  37655  icceuelpart  39974  goldbachthlem2  39996  gbegt5  40183  aacllem  42356