Theorem ancomsd 485

Description: Deduction commuting conjunction in antecedent.

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		ancomsd.1	. 2 |- (ph -> ((ps /\ ch) -> th))
2		ancom 482	. 2 |- ((ch /\ ps) <-> (ps /\ ch))
3	1, 2	syl5ib 223	1 |- (ph -> ((ch /\ ps) -> th))

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  sylan2d 507  anabsi6 554  trintss 3427  wereu 3654  ordiso 5683  cfub 6056  leltadd 6830  lemul12b 7024  lemul12aOLD 7025  iooss2 7541  znnenlem 8770  subgabl 9432  cvcon3 11856  atexch 11953  fseq1cl 13619  lbzbi 13657  dvdsadd 13688  trintssOLD 13795  axfelem14 14044  hmphtr 14885  hmeogrp 14892  ordisoOLD 15374  filssufillem 15570  unirep 15664  difxp 15690  frfi 15771  fzsplit 15792  seq1eq2 15817  iocopnst 15877  sstotbnd 15936  ismtyhmeolem 15950  heiborlem1 15955  heiborlem16 15970  heiborlem23 15977  heiborlem29 15983  heiborlem32 15986  prter2 16285  pm14.24 16397  smoel 16451  smoiun 16452  smoge 16454  posgelem 16795  lubid 16807  cvrcon3b 16994

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain