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

Theorem ancomd 452
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 451 . 2  |-  ( ( ps  /\  ch )  <->  ( ch  /\  ps )
)
31, 2sylib 199 1  |-  ( ph  ->  ( ch  /\  ps ) )
Colors of variables: wff setvar class
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:  simprd  464  jccil  542  2reu5  3280  elres  5155  relbrcnvg  5223  soxp  6916  ressuppssdif  6943  supp0cosupp0  6961  imacosupp  6962  relelec  7408  undifixp  7562  funsnfsupp  7909  infmo  8013  fpwwe2lem13  9067  nqpr  9439  infregelb  10594  hashge2el2dif  12633  ccatval3  12716  ccatsymb  12719  swrdccatin12  12837  swrdccat3  12838  cshwidxmod  12895  cshweqdif2  12908  sinbnd  14221  cosbnd  14222  lcmfun  14605  coprmgcdb  14641  ncoprmgcdne1b  14642  ncoprmlnprm  14664  vfermltl  14739  vfermltlALT  14740  modprmn0modprm0  14745  prmgaplem4  15011  prmgaplem7  15014  funcsetcestrclem8  16034  fullsetcestrc  16038  ixpsnbasval  18419  mat1dim0  19484  mat1dimid  19485  mat1dimscm  19486  mat1dimmul  19487  dmatmul  19508  scmatmats  19522  scmatscm  19524  scmatmulcl  19529  scmatcrng  19532  1marepvsma1  19594  mdet1  19612  mdet0  19617  cramerimplem1  19694  cramerimplem2  19695  cramer  19702  cpmatacl  19726  cpmatmcllem  19728  decpmatmul  19782  pmatcollpwscmatlem1  19799  pmatcollpwscmat  19801  chpmat1dlem  19845  chfacfisf  19864  chfacfscmul0  19868  chfacfpmmul0  19872  lpbl  21504  metustsym  21556  sincosq2sgn  23440  sincosq4sgn  23442  ercgrg  24548  usgra2adedgwlk  25327  usgra2adedgwlkon  25328  clwlkisclwwlklem2a  25498  eleclclwwlknlem2  25531  1to3vfriswmgra  25720  frgranbnb  25733  frgrawopreglem5  25761  frgrawopreg  25762  numclwlk1lem2fv  25806  numclwlk2lem2fv  25817  numclwwlk4  25823  numclwwlk5  25825  numclwwlk6  25826  numclwwlk7  25827  shorth  26933  trleile  28421  oddpwdc  29182  bnj1098  29590  bnj999  29763  bnj1118  29788  segcon2  30864  lsateln0  32479  cvrcmp2  32768  dalemswapyz  33139  lhprelat3N  33523  cdleme28b  33856  qirropth  35675  nzin  36524  sigaraf  38174  sigarmf  38175  sigaras  38176  sigarms  38177  sigariz  38184  afvelrn  38381  evensumeven  38545  evengpop3  38604  evengpoap3  38605  nnsum4primeseven  38606  nnsum4primesevenALTV  38607  tgoldbach  38622  proththd  38625  pfxsuffeqwrdeq  38658  ccatpfx  38661  pfxccatin12  38677  pfxccat3  38678  pfxccat3a  38681  pfxco  38690  elpwdifsn  38694  elfzelfzlble  38749  usgfislem2  39028  usgfisALTlem2  39032  mgmhmf1o  39058  rnghmf1o  39174  c0snmgmhm  39185  lmodvsmdi  39440  ply1mulgsumlem1  39451  lindslinindsimp1  39523  lindsrng01  39534  ldepspr  39539  elbigolo1  39641  digexp  39691  dig1  39692
  Copyright terms: Public domain W3C validator