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  3162  elres  5140  relbrcnvg  5202  soxp  6680  ressuppssdif  6705  supp0cosupp0  6723  imacosupp  6724  relelec  7133  undifixp  7291  funsnfsupp  7636  fpwwe2lem13  8801  nqpr  9175  hashge2el2dif  12176  ccatsymb  12273  swrdccatin12  12374  swrdccat3  12375  cshwidxmod  12432  cshweqdif2  12445  sinbnd  13456  cosbnd  13457  modprmn0modprm0  13867  ixpsnbasval  17267  1marepvsma1  18369  cramerimplem1  18464  cramerimplem2  18465  cramer  18472  lpbl  20053  metustsymOLD  20111  metustsym  20112  sincosq2sgn  21936  sincosq4sgn  21938  shorth  24649  trleile  26078  oddpwdc  26689  segcon2  28087  qirropth  29202  sigaraf  29842  sigarmf  29843  sigaras  29844  sigarms  29845  sigariz  29852  afvelrn  30027  elfzelfzlble  30162  usgra2adedgwlk  30259  usgra2adedgwlkon  30260  clwlkisclwwlklem2a  30400  eleclclwwlknlem2  30444  1to3vfriswmgra  30552  frgranbnb  30565  frgrawopreglem5  30594  frgrawopreg  30595  numclwlk1lem2fv  30639  numclwlk2lem2fv  30650  numclwwlk4  30656  numclwwlk5  30658  numclwwlk6  30659  numclwwlk7  30660  lmodvsmdi  30751  mat1dim0  30792  mat1dimid  30793  mat1dimscm  30794  mat1dimmul  30795  dmatmul  30799  scmatcrng  30811  mdet0  30822  lindslinindsimp1  30880  lindsrng01  30891  ldepspr  30896  bnj1098  31664  bnj999  31837  bnj1118  31862  lsateln0  32480  cvrcmp2  32769  dalemswapyz  33140  lhprelat3N  33524  cdleme28b  33855
  Copyright terms: Public domain W3C validator