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  3749  relbrcnvg  5968  soxp  7823  ressuppssdif  7851  supp0cosupp0OLD  7873  imacosuppOLD  7875  relelec  8334  undifixp  8498  funsnfsupp  8857  infmo  8959  fpwwe2lem13  10064  nqpr  10436  infregelb  11625  ssfzunsnext  12953  focdmex  13712  hashf1rn  13714  hashge2el2dif  13839  pfxccatin12  14095  cshwidxmod  14165  cshweqdif2  14181  pfxco  14200  sinbnd  15533  cosbnd  15534  lcmfun  15989  divgcdcoprmex  16010  cncongr1  16011  vfermltlALT  16139  setsstruct2  16521  funcsetcestrclem8  17412  fullsetcestrc  17416  smndex1iidm  18066  cyccom  18346  mat1dim0  21082  mat1dimid  21083  mat1dimscm  21084  mat1dimmul  21085  dmatmul  21106  scmatcrng  21130  1marepvsma1  21192  cramerimplem1  21292  cramerimplem2  21293  cpmatacl  21324  cpmatmcllem  21326  decpmatmul  21380  pmatcollpwscmatlem1  21397  chpmat1dlem  21443  chfacfscmul0  21466  chfacfpmmul0  21470  lpbl  23113  metustsym  23165  sincosq2sgn  25085  sincosq4sgn  25087  ercgrg  26303  subupgr  27069  nbgr2vtx1edg  27132  nbuhgr2vtx1edgb  27134  cplgr3v  27217  pthdivtx  27510  usgr2wlkspthlem1  27538  usgr2wlkspthlem2  27539  wwlknbp  27620  clwlkclwwlklem2a  27776  eleclclwwlknlem2  27840  clwwlknonwwlknonb  27885  clwlknon2num  28147  numclwlk1lem1  28148  numclwlk1lem2  28149  numclwwlk7  28170  frgrreg  28173  shorth  29072  trleile  30653  oddpwdc  31612  bnj1098  32055  bnj999  32230  bnj1118  32256  segcon2  33566  pibt2  34701  lsateln0  36146  cvrcmp2  36435  dalemswapyz  36807  lhprelat3N  37191  cdleme28b  37522  qirropth  39554  nzin  40699  sigaraf  43159  sigarmf  43160  sigaras  43161  sigarms  43162  sigariz  43169  afvelrn  43416  elfzelfzlble  43570  prproropf1olem4  43717  prprelprb  43728  fmtnoprmfac2  43778  flsqrt  43805  proththd  43828  evensumeven  43921  evengpop3  44012  evengpoap3  44013  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  tgoldbach  44031  uspgrsprfo  44072  mgmhmf1o  44103  rnghmf1o  44223  c0snmgmhm  44234  lmodvsmdi  44479  ply1mulgsumlem1  44489  lindslinindsimp1  44561  lindsrng01  44572  ldepspr  44577  digexp  44716  dig1  44717  rrx2pnedifcoorneorr  44753  rrxsphere  44784  setrec1lem3  44841