Theorem ancomsd 465

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  sylan2d  605  anabsi6  670  mpand  695  2eu3  2651  ralcom2  3345  somo  5568  wereu2  5618  smoel  8289  cfub  10150  cofsmo  10170  grudomon  10718  axpre-sup  11070  leltadd  11611  lemul12b  11988  lbzbi  12844  injresinj  13701  swrdnnn0nd  14574  abslt  15232  absle  15233  o1lo1  15454  o1co  15503  rlimno1  15571  dvdssub2  16222  lublecllem  18274  f1omvdco2  19370  ptpjpre1  23496  iocopnst  24874  ovolicc2lem4  25458  itg2le  25677  ulmcau  26341  cxpeq0  26624  pntrsumbnd2  27515  absslt  28197  cvcon3  32275  atexch  32372  abfmpeld  32647  r1filimi  35125  wsuclem  35878  btwntriv2  36067  btwnexch3  36075  isbasisrelowllem1  37410  isbasisrelowllem2  37411  relowlssretop  37418  finxpsuclem  37452  isinf2  37460  finixpnum  37655  fin2solem  37656  ltflcei  37658  poimirlem27  37697  itg2addnclem  37721  unirep  37764  prter2  38990  cvrcon3b  39386  fltaccoprm  42748  incssnn0  42818  eldioph4b  42918  fphpdo  42924  pellexlem5  42940  pm14.24  44539  traxext  45084  icceuelpart  47550  prsprel  47601  sprsymrelfolem2  47607  goldbachthlem2  47660  gbegt5  47875  aacllem  49916