Theorem ancomsd 471

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

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

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 402

This theorem is used by:  sylan2d  617  anabsi6  683  mpand  708  2eu3  2680  ralcom2  3364  somo  5606  wereu2  5656  smoel  8352  cfub  10253  cofsmo  10274  grudomon  10829  axpre-sup  11181  leltadd  11725  lemul12b  12099  lbzbi  12988  injresinj  13849  swrdnnn0nd  14728  abslt  15404  absle  15405  o1lo1  15626  o1co  15675  rlimno1  15743  dvdssub2  16395  lublecllem  18450  f1omvdco2  19579  ptpjpre1  23801  iocopnst  25172  ovolicc2lem4  25752  itg2le  25971  ulmcau  26631  cxpeq0  26916  pntrsumbnd2  27804  abslts  28515  cvcon3  32766  atexch  32863  abfmpeld  33129  r1filimi  35613  noinfepfnregs  35660  wsuclem  36404  btwntriv2  36594  btwnexch3  36602  isbasisrelowllem1  38111  isbasisrelowllem2  38112  relowlssretop  38119  finxpsuclem  38153  isinf2  38161  finixpnum  38361  fin2solem  38362  ltflcei  38364  poimirlem27  38398  itg2addnclem  38422  unirep  38466  prter2  39756  cvrcon3b  40152  fltaccoprm  43488  incssnn0  43558  eldioph4b  43654  fphpdo  43660  pellexlem5  43676  pm14.24  45258  traxext  45802  icceuelpart  48338  prsprel  48389  sprsymrelfolem2  48395  goldbachthlem2  48451  gbegt5  48679  aacllem  50774