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

Theorem ancomd 463
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 462 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2sylib 217 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  simprd  497  jccil  524  2reu5  3717  relbrcnvg  6058  soxp  8062  ressuppssdif  8117  relelec  8694  undifixp  8873  funsnfsupp  9330  infmo  9432  fpwwe2lem12  10579  nqpr  10951  infregelb  12140  ssfzunsnext  13487  hashf1rn  14253  hashge2el2dif  14380  pfxccatin12  14622  cshwidxmod  14692  cshweqdif2  14708  pfxco  14728  sinbnd  16063  cosbnd  16064  lcmfun  16522  divgcdcoprmex  16543  cncongr1  16544  vfermltlALT  16675  setsstruct2  17047  funcsetcestrclem8  18051  fullsetcestrc  18055  smndex1iidm  18712  cyccom  18997  mat1dim0  21825  mat1dimid  21826  mat1dimscm  21827  mat1dimmul  21828  dmatmul  21849  scmatcrng  21873  1marepvsma1  21935  cramerimplem1  22035  cramerimplem2  22036  cpmatacl  22068  cpmatmcllem  22070  decpmatmul  22124  pmatcollpwscmatlem1  22141  chpmat1dlem  22187  chfacfscmul0  22210  chfacfpmmul0  22214  lpbl  23862  metustsym  23914  sincosq2sgn  25859  sincosq4sgn  25861  ercgrg  27462  subupgr  28238  nbgr2vtx1edg  28301  nbuhgr2vtx1edgb  28303  cplgr3v  28386  pthdivtx  28680  usgr2wlkspthlem1  28708  usgr2wlkspthlem2  28709  wwlknbp  28790  clwlkclwwlklem2a  28945  eleclclwwlknlem2  29008  clwwlknonwwlknonb  29053  clwlknon2num  29315  numclwlk1lem1  29316  numclwlk1lem2  29317  numclwwlk7  29338  frgrreg  29341  shorth  30240  trleile  31834  oddpwdc  32957  bnj1098  33398  bnj999  33573  bnj1118  33599  segcon2  34693  pibt2  35891  lsateln0  37460  cvrcmp2  37749  dalemswapyz  38122  lhprelat3N  38506  cdleme28b  38837  qirropth  41234  onsucf1lem  41607  omlim2  41636  nzin  42605  sigaraf  45101  sigarmf  45102  sigaras  45103  sigarms  45104  sigariz  45111  f1cof1b  45316  afvelrn  45407  elfzelfzlble  45560  prproropf1olem4  45705  prprelprb  45716  fmtnoprmfac2  45766  flsqrt  45792  proththd  45813  evensumeven  45906  evengpop3  45997  evengpoap3  45998  nnsum4primeseven  45999  nnsum4primesevenALTV  46000  tgoldbach  46016  mgmhmf1o  46088  rnghmf1o  46208  c0snmgmhm  46219  lmodvsmdi  46465  ply1mulgsumlem1  46474  lindslinindsimp1  46545  lindsrng01  46556  ldepspr  46561  digexp  46700  dig1  46701  rrx2pnedifcoorneorr  46810  rrxsphere  46841  setrec1lem3  47141
  Copyright terms: Public domain W3C validator