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

Theorem ancomd 462
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 461 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2sylib 219 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  simprd  496  jccil  523  2reu5  3748  relbrcnvg  5962  soxp  7814  ressuppssdif  7842  supp0cosupp0OLD  7864  imacosuppOLD  7866  relelec  8324  undifixp  8487  funsnfsupp  8846  infmo  8948  fpwwe2lem13  10053  nqpr  10425  infregelb  11614  ssfzunsnext  12942  focdmex  13701  hashf1rn  13703  hashge2el2dif  13828  pfxccatin12  14085  cshwidxmod  14155  cshweqdif2  14171  pfxco  14190  sinbnd  15523  cosbnd  15524  lcmfun  15979  divgcdcoprmex  16000  cncongr1  16001  vfermltlALT  16129  setsstruct2  16511  funcsetcestrclem8  17402  fullsetcestrc  17406  cyccom  18286  mat1dim0  21012  mat1dimid  21013  mat1dimscm  21014  mat1dimmul  21015  dmatmul  21036  scmatcrng  21060  1marepvsma1  21122  cramerimplem1  21222  cramerimplem2  21223  cpmatacl  21254  cpmatmcllem  21256  decpmatmul  21310  pmatcollpwscmatlem1  21327  chpmat1dlem  21373  chfacfscmul0  21396  chfacfpmmul0  21400  lpbl  23042  metustsym  23094  sincosq2sgn  25014  sincosq4sgn  25016  ercgrg  26231  subupgr  26997  nbgr2vtx1edg  27060  nbuhgr2vtx1edgb  27062  cplgr3v  27145  pthdivtx  27438  usgr2wlkspthlem1  27466  usgr2wlkspthlem2  27467  wwlknbp  27548  clwlkclwwlklem2a  27704  eleclclwwlknlem2  27768  clwwlknonwwlknonb  27813  clwlknon2num  28075  numclwlk1lem1  28076  numclwlk1lem2  28077  numclwwlk7  28098  frgrreg  28101  shorth  29000  trleile  30581  oddpwdc  31512  bnj1098  31955  bnj999  32129  bnj1118  32154  segcon2  33464  pibt2  34581  lsateln0  36013  cvrcmp2  36302  dalemswapyz  36674  lhprelat3N  37058  cdleme28b  37389  qirropth  39385  nzin  40530  sigaraf  42991  sigarmf  42992  sigaras  42993  sigarms  42994  sigariz  43001  afvelrn  43248  elfzelfzlble  43402  prproropf1olem4  43515  prprelprb  43526  fmtnoprmfac2  43576  flsqrt  43603  proththd  43626  evensumeven  43719  evengpop3  43810  evengpoap3  43811  nnsum4primeseven  43812  nnsum4primesevenALTV  43813  tgoldbach  43829  uspgrsprfo  43870  mgmhmf1o  43901  smndex1iidm  43971  rnghmf1o  44072  c0snmgmhm  44083  lmodvsmdi  44328  ply1mulgsumlem1  44338  lindslinindsimp1  44410  lindsrng01  44421  ldepspr  44426  digexp  44565  dig1  44566  rrx2pnedifcoorneorr  44602  rrxsphere  44633  setrec1lem3  44690
  Copyright terms: Public domain W3C validator