Theorem ancomd 461

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

Step	Hyp	Ref	Expression
1		ancomd.1	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
2		ancom 460	. 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
3	1, 2	sylib 217	1 ⊢ (𝜑 → (𝜒 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 395

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 396

This theorem is referenced by:  simprd  495  jccil  522  2reu5  3688  relbrcnvg  6002  soxp  7941  ressuppssdif  7972  relelec  8501  undifixp  8680  funsnfsupp  9082  infmo  9184  fpwwe2lem12  10329  nqpr  10701  infregelb  11889  ssfzunsnext  13230  focdmex  13993  hashf1rn  13995  hashge2el2dif  14122  pfxccatin12  14374  cshwidxmod  14444  cshweqdif2  14460  pfxco  14479  sinbnd  15817  cosbnd  15818  lcmfun  16278  divgcdcoprmex  16299  cncongr1  16300  vfermltlALT  16431  setsstruct2  16803  funcsetcestrclem8  17795  fullsetcestrc  17799  smndex1iidm  18455  cyccom  18737  mat1dim0  21530  mat1dimid  21531  mat1dimscm  21532  mat1dimmul  21533  dmatmul  21554  scmatcrng  21578  1marepvsma1  21640  cramerimplem1  21740  cramerimplem2  21741  cpmatacl  21773  cpmatmcllem  21775  decpmatmul  21829  pmatcollpwscmatlem1  21846  chpmat1dlem  21892  chfacfscmul0  21915  chfacfpmmul0  21919  lpbl  23565  metustsym  23617  sincosq2sgn  25561  sincosq4sgn  25563  ercgrg  26782  subupgr  27557  nbgr2vtx1edg  27620  nbuhgr2vtx1edgb  27622  cplgr3v  27705  pthdivtx  27998  usgr2wlkspthlem1  28026  usgr2wlkspthlem2  28027  wwlknbp  28108  clwlkclwwlklem2a  28263  eleclclwwlknlem2  28326  clwwlknonwwlknonb  28371  clwlknon2num  28633  numclwlk1lem1  28634  numclwlk1lem2  28635  numclwwlk7  28656  frgrreg  28659  shorth  29558  trleile  31151  oddpwdc  32221  bnj1098  32663  bnj999  32838  bnj1118  32864  segcon2  34334  pibt2  35515  lsateln0  36936  cvrcmp2  37225  dalemswapyz  37597  lhprelat3N  37981  cdleme28b  38312  qirropth  40646  nzin  41825  sigaraf  44256  sigarmf  44257  sigaras  44258  sigarms  44259  sigariz  44266  f1cof1b  44456  afvelrn  44547  elfzelfzlble  44701  prproropf1olem4  44846  prprelprb  44857  fmtnoprmfac2  44907  flsqrt  44933  proththd  44954  evensumeven  45047  evengpop3  45138  evengpoap3  45139  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  tgoldbach  45157  mgmhmf1o  45229  rnghmf1o  45349  c0snmgmhm  45360  lmodvsmdi  45606  ply1mulgsumlem1  45615  lindslinindsimp1  45686  lindsrng01  45697  ldepspr  45702  digexp  45841  dig1  45842  rrx2pnedifcoorneorr  45951  rrxsphere  45982  setrec1lem3  46281