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

Theorem ancomd 466
Description: Commutation of conjuncts in consequent. (Contributed by Jeff Hankins, 14-Aug-2009.)
Hypothesis
Ref Expression
ancomd.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
ancomd (𝜑 → (𝜒𝜓))

Proof of Theorem ancomd
StepHypRef Expression
1 ancomd.1 . 2 (𝜑 → (𝜓𝜒))
2 ancom 465 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2sylib 208 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  simprd  478  jccil  562  2reu5  3449  elpwdifsn  4352  elres  5470  relbrcnvg  5539  frnssb  6431  soxp  7335  ressuppssdif  7361  supp0cosupp0  7379  imacosupp  7380  relelec  7830  undifixp  7986  funsnfsupp  8340  infmo  8442  fpwwe2lem13  9502  nqpr  9874  infregelb  11045  ssfzunsnext  12424  focdmex  13179  hashf1rn  13181  hashge2el2dif  13300  ccatval3  13397  ccatsymb  13400  ccatalpha  13411  swrdccatin12  13537  swrdccat3  13538  cshwidxmod  13595  cshweqdif2  13611  sinbnd  14954  cosbnd  14955  dvdsdivcl  15085  nn0ehalf  15142  nn0oddm1d2  15148  nnoddm1d2  15149  sumeven  15157  lcmfun  15405  coprmgcdb  15409  ncoprmgcdne1b  15410  divgcdcoprm0  15426  divgcdcoprmex  15427  cncongr1  15428  ncoprmlnprm  15483  vfermltl  15553  vfermltlALT  15554  modprmn0modprm0  15559  dvdsprmpweqle  15637  prmgaplem4  15805  prmgaplem7  15808  setsstruct2  15943  funcsetcestrclem8  16849  fullsetcestrc  16853  ixpsnbasval  19257  mat1dim0  20327  mat1dimid  20328  mat1dimscm  20329  mat1dimmul  20330  dmatmul  20351  scmatmats  20365  scmatscm  20367  scmatmulcl  20372  scmatcrng  20375  1marepvsma1  20437  mdet1  20455  mdet0  20460  cramerimplem1  20537  cramerimplem2  20538  cramer  20545  cpmatacl  20569  cpmatmcllem  20571  decpmatmul  20625  pmatcollpwscmatlem1  20642  pmatcollpwscmat  20644  chpmat1dlem  20688  chfacfisf  20707  chfacfscmul0  20711  chfacfpmmul0  20715  lpbl  22355  metustsym  22407  sincosq2sgn  24296  sincosq4sgn  24298  ercgrg  25457  subupgr  26224  usgrfilem  26264  nbgr2vtx1edg  26291  nbuhgr2vtx1edgb  26293  cplgr3v  26387  wlkreslem  26622  pthdivtx  26681  usgr2wlkspthlem1  26709  usgr2wlkspthlem2  26710  wwlknbp  26790  clwlkclwwlklem2a  26964  eleclclwwlknlem2  27026  clwwlknon1loop  27073  clwwlknonwwlknonb  27080  uhgr3cyclex  27160  eucrctshift  27221  1to3vfriswmgr  27260  frgrnbnb  27273  fusgreghash2wspv  27315  clwwlkccatlem  27331  clwwlkccat  27332  numclwwlk6  27377  numclwwlk7  27378  frgrreggt1  27380  frgrreg  27381  shorth  28282  trleile  29794  oddpwdc  30544  bnj1098  30980  bnj999  31153  bnj1118  31178  segcon2  32337  lsateln0  34600  cvrcmp2  34889  dalemswapyz  35260  lhprelat3N  35644  cdleme28b  35976  qirropth  37790  nzin  38834  sigaraf  41363  sigarmf  41364  sigaras  41365  sigarms  41366  sigariz  41373  afvelrn  41569  elfzelfzlble  41656  pfxsuffeqwrdeq  41731  ccatpfx  41734  pfxccatin12  41750  pfxccat3  41751  pfxccat3a  41754  pfxco  41763  fmtnoprmfac2  41804  flsqrt  41833  proththd  41856  evensumeven  41941  evengpop3  42011  evengpoap3  42012  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  tgoldbach  42030  tgoldbachOLD  42037  uspgrsprfo  42081  mgmhmf1o  42112  rnghmf1o  42228  c0snmgmhm  42239  lmodvsmdi  42488  ply1mulgsumlem1  42499  lindslinindsimp1  42571  lindsrng01  42582  ldepspr  42587  elbigolo1  42676  digexp  42726  dig1  42727  setrec1lem3  42761
  Copyright terms: Public domain W3C validator