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 221 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  simprd  499  jccil  526  2reu5  3697  relbrcnvg  5935  soxp  7806  ressuppssdif  7834  supp0cosupp0OLD  7856  imacosuppOLD  7858  relelec  8317  undifixp  8481  funsnfsupp  8841  infmo  8943  fpwwe2lem13  10053  nqpr  10425  infregelb  11612  ssfzunsnext  12947  focdmex  13707  hashf1rn  13709  hashge2el2dif  13834  pfxccatin12  14086  cshwidxmod  14156  cshweqdif2  14172  pfxco  14191  sinbnd  15525  cosbnd  15526  lcmfun  15979  divgcdcoprmex  16000  cncongr1  16001  vfermltlALT  16129  setsstruct2  16513  funcsetcestrclem8  17404  fullsetcestrc  17408  smndex1iidm  18058  cyccom  18338  mat1dim0  21078  mat1dimid  21079  mat1dimscm  21080  mat1dimmul  21081  dmatmul  21102  scmatcrng  21126  1marepvsma1  21188  cramerimplem1  21288  cramerimplem2  21289  cpmatacl  21321  cpmatmcllem  21323  decpmatmul  21377  pmatcollpwscmatlem1  21394  chpmat1dlem  21440  chfacfscmul0  21463  chfacfpmmul0  21467  lpbl  23110  metustsym  23162  sincosq2sgn  25092  sincosq4sgn  25094  ercgrg  26311  subupgr  27077  nbgr2vtx1edg  27140  nbuhgr2vtx1edgb  27142  cplgr3v  27225  pthdivtx  27518  usgr2wlkspthlem1  27546  usgr2wlkspthlem2  27547  wwlknbp  27628  clwlkclwwlklem2a  27783  eleclclwwlknlem2  27846  clwwlknonwwlknonb  27891  clwlknon2num  28153  numclwlk1lem1  28154  numclwlk1lem2  28155  numclwwlk7  28176  frgrreg  28179  shorth  29078  trleile  30679  oddpwdc  31722  bnj1098  32165  bnj999  32340  bnj1118  32366  segcon2  33679  pibt2  34834  lsateln0  36291  cvrcmp2  36580  dalemswapyz  36952  lhprelat3N  37336  cdleme28b  37667  qirropth  39847  nzin  41020  sigaraf  43465  sigarmf  43466  sigaras  43467  sigarms  43468  sigariz  43475  afvelrn  43722  elfzelfzlble  43876  prproropf1olem4  44021  prprelprb  44032  fmtnoprmfac2  44082  flsqrt  44108  proththd  44130  evensumeven  44223  evengpop3  44314  evengpoap3  44315  nnsum4primeseven  44316  nnsum4primesevenALTV  44317  tgoldbach  44333  uspgrsprfo  44374  mgmhmf1o  44405  rnghmf1o  44525  c0snmgmhm  44536  lmodvsmdi  44782  ply1mulgsumlem1  44792  lindslinindsimp1  44864  lindsrng01  44875  ldepspr  44880  digexp  45019  dig1  45020  rrx2pnedifcoorneorr  45129  rrxsphere  45160  setrec1lem3  45217
  Copyright terms: Public domain W3C validator