Theorem ancomd 466

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  simprd  500  jccil  531  2reu5  3724  relbrcnvg  6098  soxp  8113  ressuppssdif  8169  relelec  8730  undifixp  8920  funsnfsupp  9340  infmo  9445  fpwwe2lem12  10615  nqpr  10987  infregelb  12190  ssfzunsnext  13588  hashf1rn  14379  hashge2el2dif  14507  pfxccatin12  14760  cshwidxmod  14830  cshweqdif2  14846  pfxco  14865  sinbnd  16226  cosbnd  16227  lcmfun  16693  divgcdcoprmex  16714  cncongr1  16715  vfermltlALT  16852  setsstruct2  17224  funcsetcestrclem8  18208  fullsetcestrc  18212  chnccat  18672  mgmhmf1o  18748  smndex1iidm  18950  cyccom  19265  rnghmf1o  20525  c0snmgmhm  20535  quscrng  21385  mat1dim0  22591  mat1dimid  22592  mat1dimscm  22593  mat1dimmul  22594  dmatmul  22615  scmatcrng  22639  1marepvsma1  22701  cramerimplem1  22801  cramerimplem2  22802  cpmatacl  22834  cpmatmcllem  22836  decpmatmul  22890  pmatcollpwscmatlem1  22907  chpmat1dlem  22953  chfacfscmul0  22976  chfacfpmmul0  22980  lpbl  24621  metustsym  24673  sincosq2sgn  26622  sincosq4sgn  26624  ercgrg  28744  subupgr  29546  nbgr2vtx1edg  29609  nbuhgr2vtx1edgb  29611  cplgr3v  29694  pthdivtx  29985  usgr2wlkspthlem1  30015  usgr2wlkspthlem2  30016  wwlknbp  30100  clwlkclwwlklem2a  30258  eleclclwwlknlem2  30321  clwwlknonwwlknonb  30366  clwlknon2num  30628  numclwlk1lem1  30629  numclwlk1lem2  30630  numclwwlk7  30651  frgrreg  30654  shorth  31556  trleile  33204  oddpwdc  34661  bnj1098  35089  bnj999  35263  bnj1118  35289  segcon2  36468  pibt2  37923  lsateln0  39631  cvrcmp2  39920  dalemswapyz  40292  lhprelat3N  40676  cdleme28b  41007  qirropth  43497  onsucf1lem  43858  omlim2  43888  tfsconcatlem  43925  tfsconcatrn  43931  tfsconcatrev  43937  nzin  44892  sigaraf  47425  sigarmf  47426  sigaras  47427  sigarms  47428  sigariz  47435  f1cof1b  47669  afvelrn  47760  elfzelfzlble  47913  prproropf1olem4  48110  prprelprb  48121  fmtnoprmfac2  48174  flsqrt  48200  proththd  48221  evensumeven  48327  evengpop3  48418  evengpoap3  48419  nnsum4primeseven  48420  nnsum4primesevenALTV  48421  tgoldbach  48437  uhgrimisgrgric  48551  gpgedg2ov  48686  gpgedg2iv  48687  lmodvsmdi  49010  ply1mulgsumlem1  49017  lindslinindsimp1  49088  lindsrng01  49099  ldepspr  49104  digexp  49238  dig1  49239  rrx2pnedifcoorneorr  49348  rrxsphere  49379  setrec1lem3  50318