Theorem ancomd 464

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  simprd  498  jccil  525  2reu5  3751  relbrcnvg  5970  soxp  7825  ressuppssdif  7853  supp0cosupp0OLD  7875  imacosuppOLD  7877  relelec  8336  undifixp  8500  funsnfsupp  8859  infmo  8961  fpwwe2lem13  10066  nqpr  10438  infregelb  11627  ssfzunsnext  12955  focdmex  13714  hashf1rn  13716  hashge2el2dif  13841  pfxccatin12  14097  cshwidxmod  14167  cshweqdif2  14183  pfxco  14202  sinbnd  15535  cosbnd  15536  lcmfun  15991  divgcdcoprmex  16012  cncongr1  16013  vfermltlALT  16141  setsstruct2  16523  funcsetcestrclem8  17414  fullsetcestrc  17418  smndex1iidm  18068  cyccom  18348  mat1dim0  21084  mat1dimid  21085  mat1dimscm  21086  mat1dimmul  21087  dmatmul  21108  scmatcrng  21132  1marepvsma1  21194  cramerimplem1  21294  cramerimplem2  21295  cpmatacl  21326  cpmatmcllem  21328  decpmatmul  21382  pmatcollpwscmatlem1  21399  chpmat1dlem  21445  chfacfscmul0  21468  chfacfpmmul0  21472  lpbl  23115  metustsym  23167  sincosq2sgn  25087  sincosq4sgn  25089  ercgrg  26305  subupgr  27071  nbgr2vtx1edg  27134  nbuhgr2vtx1edgb  27136  cplgr3v  27219  pthdivtx  27512  usgr2wlkspthlem1  27540  usgr2wlkspthlem2  27541  wwlknbp  27622  clwlkclwwlklem2a  27778  eleclclwwlknlem2  27842  clwwlknonwwlknonb  27887  clwlknon2num  28149  numclwlk1lem1  28150  numclwlk1lem2  28151  numclwwlk7  28172  frgrreg  28175  shorth  29074  trleile  30655  oddpwdc  31614  bnj1098  32057  bnj999  32232  bnj1118  32258  segcon2  33568  pibt2  34700  lsateln0  36133  cvrcmp2  36422  dalemswapyz  36794  lhprelat3N  37178  cdleme28b  37509  qirropth  39512  nzin  40657  sigaraf  43117  sigarmf  43118  sigaras  43119  sigarms  43120  sigariz  43127  afvelrn  43374  elfzelfzlble  43528  prproropf1olem4  43675  prprelprb  43686  fmtnoprmfac2  43736  flsqrt  43763  proththd  43786  evensumeven  43879  evengpop3  43970  evengpoap3  43971  nnsum4primeseven  43972  nnsum4primesevenALTV  43973  tgoldbach  43989  uspgrsprfo  44030  mgmhmf1o  44061  rnghmf1o  44181  c0snmgmhm  44192  lmodvsmdi  44437  ply1mulgsumlem1  44447  lindslinindsimp1  44519  lindsrng01  44530  ldepspr  44535  digexp  44674  dig1  44675  rrx2pnedifcoorneorr  44711  rrxsphere  44742  setrec1lem3  44799