HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

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
StepHypRef Expression
1 ancomsd.1 . 2 |- (ph -> ((ps /\ ch) -> th))
2 ancom 482 . 2 |- ((ch /\ ps) <-> (ps /\ ch))
31, 2syl5ib 223 1 |- (ph -> ((ch /\ ps) -> th))
Colors of variables: wff set class
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