Theorem ancomsd 455

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 451	. 2 |- ( ( ch /\ ps ) <-> ( ps /\ ch ) )
2		ancomsd.1	. 2 |- ( ph -> ( ( ps /\ ch ) -> th ) )
3	1, 2	syl5bi 220	1 |- ( ph -> ( ( ch /\ ps ) -> th ) )

Syntax hints:   -> wi 4   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  sylan2d  484  mpand  679  anabsi6  825  ralcom2  2927  ralxfrd  4573  somo  4746  wereu2  4788  poirr2  5181  ordtr3  5425  smoel  7029  cfub  8625  cofsmo  8645  grudomon  9188  axpre-sup  9539  leltadd  10044  lemul12b  10408  lbzbi  11198  injresinj  11970  abslt  13316  absle  13317  o1lo1  13539  o1co  13588  rlimno1  13655  znnenlem  14202  dvdssub2  14280  lublecllem  16172  f1omvdco2  17027  ptpjpre1  20523  iocopnst  21905  ovolicc2lem4OLD  22410  ovolicc2lem4  22411  itg2le  22634  ulmcau  23287  cxpeq0  23560  pntrsumbnd2  24342  cvcon3  27874  atexch  27971  abfmpeld  28194  wsuclem  30454  nofulllem5  30539  btwntriv2  30723  btwnexch3  30731  isbasisrelowllem1  31665  isbasisrelowllem2  31666  relowlssretop  31673  finxpsuclem  31696  finixpnum  31837  fin2solem  31838  ltflcei  31840  poimirlem27  31874  itg2addnclem  31900  unirep  31946  prter2  32364  cvrcon3b  32755  incssnn0  35465  eldioph4b  35566  fphpdo  35572  pellexlem5  35590  pm14.24  36696  icceuelpart  38563  gbegt5  38675  aacllem  40133