Theorem ancomd 453

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

Syntax hints:   → wi 4   ∧ wa 382

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 197  df-an 383

This theorem is referenced by:  simprd  483  jccil  512  2reu5  3568  elpwdifsn  4456  elres  5576  relbrcnvg  5645  frnssb  6533  soxp  7441  ressuppssdif  7467  supp0cosupp0  7486  imacosupp  7487  relelec  7939  undifixp  8098  funsnfsupp  8455  infmo  8557  fpwwe2lem13  9666  nqpr  10038  infregelb  11209  ssfzunsnext  12593  focdmex  13343  hashf1rn  13345  hashge2el2dif  13464  ccatval3  13561  ccatsymb  13564  ccatalpha  13575  swrdccatin12  13700  swrdccat3  13701  cshwidxmod  13758  cshweqdif2  13774  sinbnd  15116  cosbnd  15117  dvdsdivcl  15247  nn0ehalf  15303  nn0oddm1d2  15309  nnoddm1d2  15310  sumeven  15318  lcmfun  15566  coprmgcdb  15570  ncoprmgcdne1b  15571  divgcdcoprm0  15586  divgcdcoprmex  15587  cncongr1  15588  ncoprmlnprm  15643  vfermltl  15713  vfermltlALT  15714  modprmn0modprm0  15719  dvdsprmpweqle  15797  prmgaplem4  15965  prmgaplem7  15968  setsstruct2  16103  funcsetcestrclem8  17010  fullsetcestrc  17014  ixpsnbasval  19424  mat1dim0  20497  mat1dimid  20498  mat1dimscm  20499  mat1dimmul  20500  dmatmul  20521  scmatmats  20535  scmatscm  20537  scmatmulcl  20542  scmatcrng  20545  1marepvsma1  20607  mdet1  20625  mdet0  20630  cramerimplem1  20708  cramerimplem1OLD  20709  cramerimplem2  20710  cramer  20717  cpmatacl  20741  cpmatmcllem  20743  decpmatmul  20797  pmatcollpwscmatlem1  20814  pmatcollpwscmat  20816  chpmat1dlem  20860  chfacfisf  20879  chfacfscmul0  20883  chfacfpmmul0  20887  lpbl  22528  metustsym  22580  sincosq2sgn  24472  sincosq4sgn  24474  ercgrg  25633  subupgr  26402  usgrfilem  26442  nbgr2vtx1edg  26469  nbuhgr2vtx1edgb  26471  cplgr3v  26566  wlkreslem  26801  pthdivtx  26860  usgr2wlkspthlem1  26888  usgr2wlkspthlem2  26889  wwlknbp  26970  clwwlkccatlem  27139  clwwlkccat  27140  clwlkclwwlklem2a  27148  eleclclwwlknlem2  27219  clwwlknon1loop  27273  clwwlknonwwlknonb  27281  uhgr3cyclex  27362  eucrctshift  27423  1to3vfriswmgr  27462  frgrnbnb  27475  fusgreghash2wspv  27517  clwlknon2num  27559  numclwlk1lem1  27560  numclwlk1lem2  27561  numclwwlk6  27589  numclwwlk7  27590  frgrreggt1  27592  frgrreg  27593  shorth  28494  trleile  30006  oddpwdc  30756  bnj1098  31192  bnj999  31365  bnj1118  31390  segcon2  32549  lsateln0  34804  cvrcmp2  35093  dalemswapyz  35464  lhprelat3N  35848  cdleme28b  36180  qirropth  37999  nzin  39043  sigaraf  41562  sigarmf  41563  sigaras  41564  sigarms  41565  sigariz  41572  afvelrn  41768  elfzelfzlble  41859  pfxsuffeqwrdeq  41934  ccatpfx  41937  pfxccatin12  41953  pfxccat3  41954  pfxccat3a  41957  pfxco  41966  fmtnoprmfac2  42007  flsqrt  42036  proththd  42059  evensumeven  42144  evengpop3  42214  evengpoap3  42215  nnsum4primeseven  42216  nnsum4primesevenALTV  42217  tgoldbach  42233  tgoldbachOLD  42240  uspgrsprfo  42284  mgmhmf1o  42315  rnghmf1o  42431  c0snmgmhm  42442  lmodvsmdi  42691  ply1mulgsumlem1  42702  lindslinindsimp1  42774  lindsrng01  42785  ldepspr  42790  elbigolo1  42879  digexp  42929  dig1  42930  setrec1lem3  42964