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

Theorem ancomd 465
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 464 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2sylib 206 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  simprd  477  jccil  560  2reu5  3382  elres  5342  relbrcnvg  5410  frnssb  6283  soxp  7154  ressuppssdif  7180  supp0cosupp0  7198  imacosupp  7199  relelec  7651  undifixp  7807  funsnfsupp  8159  infmo  8261  fpwwe2lem13  9320  nqpr  9692  infregelb  10854  ssfzunsn  12212  focdmex  12953  hashf1rn  12956  hashge2el2dif  13067  ccatval3  13162  ccatsymb  13165  ccatalpha  13174  swrdccatin12  13288  swrdccat3  13289  cshwidxmod  13346  cshweqdif2  13362  sinbnd  14695  cosbnd  14696  dvdsdivcl  14822  nn0ehalf  14879  nn0oddm1d2  14885  nnoddm1d2  14886  sumeven  14894  lcmfun  15142  coprmgcdb  15146  ncoprmgcdne1b  15147  divgcdcoprm0  15163  divgcdcoprmex  15164  cncongr1  15165  ncoprmlnprm  15220  vfermltl  15290  vfermltlALT  15291  modprmn0modprm0  15296  dvdsprmpweqle  15374  prmgaplem4  15542  prmgaplem7  15545  funcsetcestrclem8  16571  fullsetcestrc  16575  ixpsnbasval  18976  mat1dim0  20040  mat1dimid  20041  mat1dimscm  20042  mat1dimmul  20043  dmatmul  20064  scmatmats  20078  scmatscm  20080  scmatmulcl  20085  scmatcrng  20088  1marepvsma1  20150  mdet1  20168  mdet0  20173  cramerimplem1  20250  cramerimplem2  20251  cramer  20258  cpmatacl  20282  cpmatmcllem  20284  decpmatmul  20338  pmatcollpwscmatlem1  20355  pmatcollpwscmat  20357  chpmat1dlem  20401  chfacfisf  20420  chfacfscmul0  20424  chfacfpmmul0  20428  lpbl  22059  metustsym  22111  sincosq2sgn  23972  sincosq4sgn  23974  lgsqrmodndvds  24795  ercgrg  25130  usgra2adedgwlk  25908  usgra2adedgwlkon  25909  clwlkisclwwlklem2a  26079  eleclclwwlknlem2  26112  1to3vfriswmgra  26300  frgranbnb  26313  frgrawopreglem5  26341  frgrawopreg  26342  numclwlk1lem2fv  26386  numclwlk2lem2fv  26397  numclwwlk4  26403  numclwwlk5  26405  numclwwlk6  26406  numclwwlk7  26407  shorth  27344  trleile  28803  oddpwdc  29549  bnj1098  29914  bnj999  30087  bnj1118  30112  segcon2  31188  lsateln0  33096  cvrcmp2  33385  dalemswapyz  33756  lhprelat3N  34140  cdleme28b  34473  qirropth  36287  nzin  37335  sigaraf  39488  sigarmf  39489  sigaras  39490  sigarms  39491  sigariz  39498  afvelrn  39695  fmtnoprmfac2  39815  flsqrt  39844  proththd  39867  evensumeven  39952  evengpop3  40012  evengpoap3  40013  nnsum4primeseven  40014  nnsum4primesevenALTV  40015  tgoldbach  40030  tgoldbachOLD  40037  pfxsuffeqwrdeq  40067  ccatpfx  40070  pfxccatin12  40086  pfxccat3  40087  pfxccat3a  40090  pfxco  40099  elpwdifsn  40110  elfzelfzlble  40178  subupgr  40506  usgrfilem  40541  nbgr2vtx1edg  40567  nbuhgr2vtx1edgb  40569  cplgr3v  40652  1wlkreslem  40873  pthdivtx  40930  usgr2wlkspthlem1  40958  usgr2wlkspthlem2  40959  wwlknbp  41039  clwwlknbp0  41187  clwlkclwwlklem2a  41202  clwwlksnfi  41215  eleclclwwlksnlem2  41241  uhgr3cyclex  41344  eucrctshift  41406  1to3vfriswmgr  41445  frgrnbnb  41458  frgrwopreglem2  41477  frgrwopreglem5  41480  frgrwopreg  41481  fusgr2wsp2nb  41493  fusgreghash2wspv  41494  av-numclwwlk4  41535  av-numclwwlk6  41539  av-numclwwlk7  41540  av-frgrareggt1  41542  av-frgrareg  41543  mgmhmf1o  41572  rnghmf1o  41688  c0snmgmhm  41699  lmodvsmdi  41952  ply1mulgsumlem1  41963  lindslinindsimp1  42035  lindsrng01  42046  ldepspr  42051  elbigolo1  42144  digexp  42194  dig1  42195
  Copyright terms: Public domain W3C validator