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 218	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 207  df-an 396

This theorem is referenced by:  simprd  495  jccil  522  2reu5  3741  relbrcnvg  6092  soxp  8128  ressuppssdif  8184  relelec  8766  undifixp  8948  funsnfsupp  9404  infmo  9509  fpwwe2lem12  10656  nqpr  11028  infregelb  12226  ssfzunsnext  13586  hashf1rn  14370  hashge2el2dif  14498  pfxccatin12  14751  cshwidxmod  14821  cshweqdif2  14837  pfxco  14857  sinbnd  16198  cosbnd  16199  lcmfun  16664  divgcdcoprmex  16685  cncongr1  16686  vfermltlALT  16822  setsstruct2  17193  funcsetcestrclem8  18174  fullsetcestrc  18178  mgmhmf1o  18678  smndex1iidm  18879  cyccom  19186  rnghmf1o  20412  c0snmgmhm  20422  quscrng  21244  mat1dim0  22411  mat1dimid  22412  mat1dimscm  22413  mat1dimmul  22414  dmatmul  22435  scmatcrng  22459  1marepvsma1  22521  cramerimplem1  22621  cramerimplem2  22622  cpmatacl  22654  cpmatmcllem  22656  decpmatmul  22710  pmatcollpwscmatlem1  22727  chpmat1dlem  22773  chfacfscmul0  22796  chfacfpmmul0  22800  lpbl  24442  metustsym  24494  sincosq2sgn  26460  sincosq4sgn  26462  ercgrg  28496  subupgr  29266  nbgr2vtx1edg  29329  nbuhgr2vtx1edgb  29331  cplgr3v  29414  pthdivtx  29709  usgr2wlkspthlem1  29739  usgr2wlkspthlem2  29740  wwlknbp  29824  clwlkclwwlklem2a  29979  eleclclwwlknlem2  30042  clwwlknonwwlknonb  30087  clwlknon2num  30349  numclwlk1lem1  30350  numclwlk1lem2  30351  numclwwlk7  30372  frgrreg  30375  shorth  31276  trleile  32951  oddpwdc  34386  bnj1098  34814  bnj999  34989  bnj1118  35015  segcon2  36123  pibt2  37435  lsateln0  39013  cvrcmp2  39302  dalemswapyz  39675  lhprelat3N  40059  cdleme28b  40390  qirropth  42931  onsucf1lem  43293  omlim2  43323  tfsconcatlem  43360  tfsconcatrn  43366  tfsconcatrev  43372  nzin  44342  sigaraf  46882  sigarmf  46883  sigaras  46884  sigarms  46885  sigariz  46892  f1cof1b  47106  afvelrn  47197  elfzelfzlble  47350  prproropf1olem4  47520  prprelprb  47531  fmtnoprmfac2  47581  flsqrt  47607  proththd  47628  evensumeven  47721  evengpop3  47812  evengpoap3  47813  nnsum4primeseven  47814  nnsum4primesevenALTV  47815  tgoldbach  47831  uhgrimisgrgric  47944  lmodvsmdi  48354  ply1mulgsumlem1  48362  lindslinindsimp1  48433  lindsrng01  48444  ldepspr  48449  digexp  48587  dig1  48588  rrx2pnedifcoorneorr  48697  rrxsphere  48728  setrec1lem3  49553