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 207 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 196  df-an 385
This theorem is referenced by:  simprd  478  jccil  561  2reu5  3383  elres  5355  relbrcnvg  5423  frnssb  6298  soxp  7177  ressuppssdif  7203  supp0cosupp0  7221  imacosupp  7222  relelec  7674  undifixp  7830  funsnfsupp  8182  infmo  8284  fpwwe2lem13  9343  nqpr  9715  infregelb  10884  ssfzunsn  12257  focdmex  13001  hashf1rn  13004  hashge2el2dif  13117  ccatval3  13216  ccatsymb  13219  ccatalpha  13228  swrdccatin12  13342  swrdccat3  13343  cshwidxmod  13400  cshweqdif2  13416  sinbnd  14749  cosbnd  14750  dvdsdivcl  14876  nn0ehalf  14933  nn0oddm1d2  14939  nnoddm1d2  14940  sumeven  14948  lcmfun  15196  coprmgcdb  15200  ncoprmgcdne1b  15201  divgcdcoprm0  15217  divgcdcoprmex  15218  cncongr1  15219  ncoprmlnprm  15274  vfermltl  15344  vfermltlALT  15345  modprmn0modprm0  15350  dvdsprmpweqle  15428  prmgaplem4  15596  prmgaplem7  15599  funcsetcestrclem8  16625  fullsetcestrc  16629  ixpsnbasval  19030  mat1dim0  20098  mat1dimid  20099  mat1dimscm  20100  mat1dimmul  20101  dmatmul  20122  scmatmats  20136  scmatscm  20138  scmatmulcl  20143  scmatcrng  20146  1marepvsma1  20208  mdet1  20226  mdet0  20231  cramerimplem1  20308  cramerimplem2  20309  cramer  20316  cpmatacl  20340  cpmatmcllem  20342  decpmatmul  20396  pmatcollpwscmatlem1  20413  pmatcollpwscmat  20415  chpmat1dlem  20459  chfacfisf  20478  chfacfscmul0  20482  chfacfpmmul0  20486  lpbl  22118  metustsym  22170  sincosq2sgn  24055  sincosq4sgn  24057  lgsqrmodndvds  24878  ercgrg  25212  usgra2adedgwlk  26142  usgra2adedgwlkon  26143  clwlkisclwwlklem2a  26313  eleclclwwlknlem2  26346  1to3vfriswmgra  26534  frgranbnb  26547  frgrawopreglem5  26575  frgrawopreg  26576  numclwlk1lem2fv  26620  numclwlk2lem2fv  26631  numclwwlk4  26637  numclwwlk5  26639  numclwwlk6  26640  numclwwlk7  26641  shorth  27538  trleile  28997  oddpwdc  29743  bnj1098  30108  bnj999  30281  bnj1118  30306  segcon2  31382  lsateln0  33300  cvrcmp2  33589  dalemswapyz  33960  lhprelat3N  34344  cdleme28b  34677  qirropth  36491  nzin  37539  sigaraf  39691  sigarmf  39692  sigaras  39693  sigarms  39694  sigariz  39701  afvelrn  39897  fmtnoprmfac2  40017  flsqrt  40046  proththd  40069  evensumeven  40154  evengpop3  40214  evengpoap3  40215  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  tgoldbach  40232  tgoldbachOLD  40239  pfxsuffeqwrdeq  40269  ccatpfx  40272  pfxccatin12  40288  pfxccat3  40289  pfxccat3a  40292  pfxco  40301  elpwdifsn  40312  elfzelfzlble  40358  subupgr  40511  usgrfilem  40546  nbgr2vtx1edg  40572  nbuhgr2vtx1edgb  40574  cplgr3v  40657  1wlkreslem  40878  pthdivtx  40935  usgr2wlkspthlem1  40963  usgr2wlkspthlem2  40964  wwlknbp  41044  clwwlknbp0  41192  clwlkclwwlklem2a  41207  clwwlksnfi  41220  eleclclwwlksnlem2  41246  uhgr3cyclex  41349  eucrctshift  41411  1to3vfriswmgr  41450  frgrnbnb  41463  frgrwopreglem2  41482  frgrwopreglem5  41485  frgrwopreg  41486  fusgr2wsp2nb  41498  fusgreghash2wspv  41499  av-numclwwlk4  41540  av-numclwwlk6  41544  av-numclwwlk7  41545  av-frgrareggt1  41547  av-frgrareg  41548  mgmhmf1o  41577  rnghmf1o  41693  c0snmgmhm  41704  lmodvsmdi  41957  ply1mulgsumlem1  41968  lindslinindsimp1  42040  lindsrng01  42051  ldepspr  42056  elbigolo1  42149  digexp  42199  dig1  42200  setrec1lem3  42235
  Copyright terms: Public domain W3C validator