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

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

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 206  df-an 397

This theorem is referenced by:  simprd  496  jccil  523  2reu5  3719  relbrcnvg  6062  soxp  8066  ressuppssdif  8121  relelec  8700  undifixp  8879  funsnfsupp  9338  infmo  9440  fpwwe2lem12  10587  nqpr  10959  infregelb  12148  ssfzunsnext  13496  hashf1rn  14262  hashge2el2dif  14391  pfxccatin12  14633  cshwidxmod  14703  cshweqdif2  14719  pfxco  14739  sinbnd  16073  cosbnd  16074  lcmfun  16532  divgcdcoprmex  16553  cncongr1  16554  vfermltlALT  16685  setsstruct2  17057  funcsetcestrclem8  18064  fullsetcestrc  18068  smndex1iidm  18725  cyccom  19010  mat1dim0  21859  mat1dimid  21860  mat1dimscm  21861  mat1dimmul  21862  dmatmul  21883  scmatcrng  21907  1marepvsma1  21969  cramerimplem1  22069  cramerimplem2  22070  cpmatacl  22102  cpmatmcllem  22104  decpmatmul  22158  pmatcollpwscmatlem1  22175  chpmat1dlem  22221  chfacfscmul0  22244  chfacfpmmul0  22248  lpbl  23896  metustsym  23948  sincosq2sgn  25893  sincosq4sgn  25895  ercgrg  27522  subupgr  28298  nbgr2vtx1edg  28361  nbuhgr2vtx1edgb  28363  cplgr3v  28446  pthdivtx  28740  usgr2wlkspthlem1  28768  usgr2wlkspthlem2  28769  wwlknbp  28850  clwlkclwwlklem2a  29005  eleclclwwlknlem2  29068  clwwlknonwwlknonb  29113  clwlknon2num  29375  numclwlk1lem1  29376  numclwlk1lem2  29377  numclwwlk7  29398  frgrreg  29401  shorth  30300  trleile  31901  oddpwdc  33043  bnj1098  33484  bnj999  33659  bnj1118  33685  segcon2  34766  pibt2  35961  lsateln0  37530  cvrcmp2  37819  dalemswapyz  38192  lhprelat3N  38576  cdleme28b  38907  qirropth  41289  onsucf1lem  41662  omlim2  41692  tfsconcatlem  41729  tfsconcatrn  41735  tfsconcatrev  41741  nzin  42720  sigaraf  45214  sigarmf  45215  sigaras  45216  sigarms  45217  sigariz  45224  f1cof1b  45429  afvelrn  45520  elfzelfzlble  45673  prproropf1olem4  45818  prprelprb  45829  fmtnoprmfac2  45879  flsqrt  45905  proththd  45926  evensumeven  46019  evengpop3  46110  evengpoap3  46111  nnsum4primeseven  46112  nnsum4primesevenALTV  46113  tgoldbach  46129  mgmhmf1o  46201  rnghmf1o  46321  c0snmgmhm  46332  lmodvsmdi  46578  ply1mulgsumlem1  46587  lindslinindsimp1  46658  lindsrng01  46669  ldepspr  46674  digexp  46813  dig1  46814  rrx2pnedifcoorneorr  46923  rrxsphere  46954  setrec1lem3  47254