Theorem ancomsd 454

Description: Deduction commuting conjunction in antecedent. (Contributed by NM, 12-Dec-2004.)

Hypothesis

Ref	Expression
ancomsd.1	|- ( ph -> ( ( ps /\ ch ) -> th ) )

Assertion

Ref	Expression
ancomsd	|- ( ph -> ( ( ch /\ ps ) -> th ) )

Proof of Theorem ancomsd

Step	Hyp	Ref	Expression
1		ancom 450	. 2 |- ( ( ch /\ ps ) <-> ( ps /\ ch ) )
2		ancomsd.1	. 2 |- ( ph -> ( ( ps /\ ch ) -> th ) )
3	1, 2	syl5bi 217	1 |- ( ph -> ( ( ch /\ ps ) -> th ) )

Syntax hints:   -> wi 4   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  sylan2d  482  mpand  675  anabsi6  816  ralcom2  3031  ralxfrd  4667  somo  4840  wereu2  4882  ordtr3  4929  poirr2  5397  smoel  7043  cfub  8641  cofsmo  8661  grudomon  9207  axpre-sup  9558  leltadd  10048  lemul12b  10411  lbzbi  11182  injresinj  11906  abslt  13127  absle  13128  o1lo1  13340  o1co  13389  rlimno1  13456  znnenlem  13823  dvdssub2  13899  lublecllem  15492  f1omvdco2  16346  ptpjpre1  19940  iocopnst  21308  ovolicc2lem4  21799  itg2le  22014  ulmcau  22657  cxpeq0  22925  pntrsumbnd2  23618  cvcon3  27026  atexch  27123  abfmpeld  27315  wsuclem  29308  nofulllem5  29393  btwntriv2  29589  btwnexch3  29597  finixpnum  29965  fin2solem  29966  ltflcei  29970  itg2addnclem  29993  unirep  30130  prter2  30550  incssnn0  30571  eldioph4b  30673  fphpdo  30679  pellexlem5  30697  pm14.24  31241  cvrcon3b  34475