Theorem ancomd 451

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

Syntax hints:   → wi 4   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  simprd  485  jccil  514  2reu5  3611  elpwdifsn  4508  elresOLD  5636  relbrcnvg  5711  frnssb  6610  soxp  7521  ressuppssdif  7547  supp0cosupp0  7566  imacosupp  7567  relelec  8019  undifixp  8178  funsnfsupp  8535  infmo  8637  fpwwe2lem13  9746  nqpr  10118  infregelb  11289  ssfzunsnext  12605  focdmex  13355  hashf1rn  13357  hashge2el2dif  13475  ccatval3  13572  ccatsymb  13575  ccatalpha  13586  swrdccatin12  13711  swrdccat3  13712  cshwidxmod  13769  cshweqdif2  13785  sinbnd  15126  cosbnd  15127  dvdsdivcl  15257  nn0ehalf  15311  nn0oddm1d2  15317  nnoddm1d2  15318  sumeven  15326  lcmfun  15573  coprmgcdb  15577  ncoprmgcdne1b  15578  divgcdcoprm0  15593  divgcdcoprmex  15594  cncongr1  15595  ncoprmlnprm  15649  vfermltl  15719  vfermltlALT  15720  modprmn0modprm0  15725  dvdsprmpweqle  15803  prmgaplem4  15971  prmgaplem7  15974  setsstruct2  16103  funcsetcestrclem8  17003  fullsetcestrc  17007  ixpsnbasval  19414  mat1dim0  20486  mat1dimid  20487  mat1dimscm  20488  mat1dimmul  20489  dmatmul  20510  scmatmats  20524  scmatscm  20526  scmatmulcl  20531  scmatcrng  20534  1marepvsma1  20596  mdet1  20614  mdet0  20619  cramerimplem1  20697  cramerimplem1OLD  20698  cramerimplem2  20699  cramer  20706  cpmatacl  20730  cpmatmcllem  20732  decpmatmul  20786  pmatcollpwscmatlem1  20803  pmatcollpwscmat  20805  chpmat1dlem  20849  chfacfisf  20868  chfacfscmul0  20872  chfacfpmmul0  20876  lpbl  22517  metustsym  22569  sincosq2sgn  24462  sincosq4sgn  24464  ercgrg  25622  subupgr  26391  usgrfilem  26431  nbgr2vtx1edg  26458  nbuhgr2vtx1edgb  26460  cplgr3v  26555  wlkreslem  26790  pthdivtx  26849  usgr2wlkspthlem1  26877  usgr2wlkspthlem2  26878  wwlknbp  26959  clwwlkccatlem  27128  clwwlkccat  27129  clwlkclwwlklem2a  27137  eleclclwwlknlem2  27208  clwwlknon1loop  27262  clwwlknonwwlknonb  27270  uhgr3cyclex  27351  eucrctshift  27412  1to3vfriswmgr  27451  frgrnbnb  27464  fusgreghash2wspv  27506  clwlknon2num  27544  numclwlk1lem1  27545  numclwlk1lem2  27546  numclwwlk6  27574  numclwwlk7  27575  frgrreggt1  27577  frgrreg  27578  shorth  28479  trleile  29988  oddpwdc  30738  bnj1098  31174  bnj999  31347  bnj1118  31372  segcon2  32530  lsateln0  34772  cvrcmp2  35061  dalemswapyz  35433  lhprelat3N  35817  cdleme28b  36149  qirropth  37971  nzin  39014  sigaraf  41521  sigarmf  41522  sigaras  41523  sigarms  41524  sigariz  41531  afvelrn  41754  elfzelfzlble  41903  pfxsuffeqwrdeq  41978  ccatpfx  41981  pfxccatin12  41997  pfxccat3  41998  pfxccat3a  42001  pfxco  42010  fmtnoprmfac2  42051  flsqrt  42080  proththd  42103  evensumeven  42188  evengpop3  42258  evengpoap3  42259  nnsum4primeseven  42260  nnsum4primesevenALTV  42261  tgoldbach  42277  uspgrsprfo  42321  mgmhmf1o  42352  rnghmf1o  42468  c0snmgmhm  42479  lmodvsmdi  42728  ply1mulgsumlem1  42739  lindslinindsimp1  42811  lindsrng01  42822  ldepspr  42827  elbigolo1  42916  digexp  42966  dig1  42967  setrec1lem3  43001