Theorem ancomd 460

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 459	. 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
3	1, 2	sylib 217	1 ⊢ (𝜑 → (𝜒 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  simprd  494  jccil  521  2reu5  3755  relbrcnvg  6105  soxp  8119  ressuppssdif  8174  relelec  8752  undifixp  8932  funsnfsupp  9391  infmo  9494  fpwwe2lem12  10641  nqpr  11013  infregelb  12204  ssfzunsnext  13552  hashf1rn  14318  hashge2el2dif  14447  pfxccatin12  14689  cshwidxmod  14759  cshweqdif2  14775  pfxco  14795  sinbnd  16129  cosbnd  16130  lcmfun  16588  divgcdcoprmex  16609  cncongr1  16610  vfermltlALT  16741  setsstruct2  17113  funcsetcestrclem8  18120  fullsetcestrc  18124  mgmhmf1o  18627  smndex1iidm  18820  cyccom  19120  rnghmf1o  20345  c0snmgmhm  20355  quscrng  21031  mat1dim0  22197  mat1dimid  22198  mat1dimscm  22199  mat1dimmul  22200  dmatmul  22221  scmatcrng  22245  1marepvsma1  22307  cramerimplem1  22407  cramerimplem2  22408  cpmatacl  22440  cpmatmcllem  22442  decpmatmul  22496  pmatcollpwscmatlem1  22513  chpmat1dlem  22559  chfacfscmul0  22582  chfacfpmmul0  22586  lpbl  24234  metustsym  24286  sincosq2sgn  26243  sincosq4sgn  26245  ercgrg  28033  subupgr  28809  nbgr2vtx1edg  28872  nbuhgr2vtx1edgb  28874  cplgr3v  28957  pthdivtx  29251  usgr2wlkspthlem1  29279  usgr2wlkspthlem2  29280  wwlknbp  29361  clwlkclwwlklem2a  29516  eleclclwwlknlem2  29579  clwwlknonwwlknonb  29624  clwlknon2num  29886  numclwlk1lem1  29887  numclwlk1lem2  29888  numclwwlk7  29909  frgrreg  29912  shorth  30813  trleile  32406  oddpwdc  33649  bnj1098  34090  bnj999  34265  bnj1118  34291  segcon2  35379  pibt2  36603  lsateln0  38170  cvrcmp2  38459  dalemswapyz  38832  lhprelat3N  39216  cdleme28b  39547  qirropth  41950  onsucf1lem  42323  omlim2  42353  tfsconcatlem  42390  tfsconcatrn  42396  tfsconcatrev  42402  nzin  43381  sigaraf  45869  sigarmf  45870  sigaras  45871  sigarms  45872  sigariz  45879  f1cof1b  46085  afvelrn  46176  elfzelfzlble  46329  prproropf1olem4  46474  prprelprb  46485  fmtnoprmfac2  46535  flsqrt  46561  proththd  46582  evensumeven  46675  evengpop3  46766  evengpoap3  46767  nnsum4primeseven  46768  nnsum4primesevenALTV  46769  tgoldbach  46785  lmodvsmdi  47148  ply1mulgsumlem1  47156  lindslinindsimp1  47227  lindsrng01  47238  ldepspr  47243  digexp  47382  dig1  47383  rrx2pnedifcoorneorr  47492  rrxsphere  47523  setrec1lem3  47823