MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ancomd Structured version   Unicode version

Theorem ancomd 451
Description: Commutation of conjuncts in consequent. (Contributed by Jeff Hankins, 14-Aug-2009.)
Hypothesis
Ref Expression
ancomd.1  |-  ( ph  ->  ( ps  /\  ch ) )
Assertion
Ref Expression
ancomd  |-  ( ph  ->  ( ch  /\  ps ) )

Proof of Theorem ancomd
StepHypRef Expression
1 ancomd.1 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
2 ancom 450 . 2  |-  ( ( ps  /\  ch )  <->  ( ch  /\  ps )
)
31, 2sylib 196 1  |-  ( ph  ->  ( ch  /\  ps ) )
Colors of variables: wff setvar class
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:  simprd  463  jccil  540  2reu5  3317  elres  5315  relbrcnvg  5381  soxp  6908  ressuppssdif  6933  supp0cosupp0  6951  imacosupp  6952  relelec  7364  undifixp  7517  funsnfsupp  7865  fpwwe2lem13  9032  nqpr  9404  hashge2el2dif  12502  ccatsymb  12580  swrdccatin12  12696  swrdccat3  12697  cshwidxmod  12754  cshweqdif2  12767  sinbnd  13793  cosbnd  13794  modprmn0modprm0  14208  ixpsnbasval  17726  mat1dim0  18844  mat1dimid  18845  mat1dimscm  18846  mat1dimmul  18847  dmatmul  18868  scmatmats  18882  scmatscm  18884  scmatmulcl  18889  scmatcrng  18892  1marepvsma1  18954  mdet1  18972  mdet0  18977  cramerimplem1  19054  cramerimplem2  19055  cramer  19062  cpmatacl  19086  cpmatmcllem  19088  decpmatmul  19142  pmatcollpwscmatlem1  19159  pmatcollpwscmat  19161  chpmat1dlem  19205  chfacfisf  19224  chfacfscmul0  19228  chfacfpmmul0  19232  lpbl  20874  metustsymOLD  20932  metustsym  20933  sincosq2sgn  22758  sincosq4sgn  22760  usgra2adedgwlk  24437  usgra2adedgwlkon  24438  clwlkisclwwlklem2a  24608  eleclclwwlknlem2  24641  1to3vfriswmgra  24830  frgranbnb  24843  frgrawopreglem5  24872  frgrawopreg  24873  numclwlk1lem2fv  24917  numclwlk2lem2fv  24928  numclwwlk4  24934  numclwwlk5  24936  numclwwlk6  24937  numclwwlk7  24938  shorth  26036  trleile  27478  oddpwdc  28118  segcon2  29682  qirropth  30772  nzin  31147  fzisoeu  31400  cncfiooicclem1  31555  fourierdlem103  31833  sigaraf  31860  sigarmf  31861  sigaras  31862  sigarms  31863  sigariz  31870  afvelrn  32043  elpwdifsn  32086  elfzelfzlble  32127  usgfislem2  32235  usgfisALTlem2  32239  lmodvsmdi  32457  ply1mulgsumlem1  32468  lindslinindsimp1  32540  lindsrng01  32551  ldepspr  32556  bnj1098  33322  bnj999  33495  bnj1118  33520  lsateln0  34193  cvrcmp2  34482  dalemswapyz  34853  lhprelat3N  35237  cdleme28b  35568
  Copyright terms: Public domain W3C validator