Theorem ancomd 465

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  simprd  499  jccil  526  2reu5  3660  relbrcnvg  5953  soxp  7874  ressuppssdif  7905  relelec  8414  undifixp  8593  funsnfsupp  8987  infmo  9089  fpwwe2lem12  10221  nqpr  10593  infregelb  11781  ssfzunsnext  13122  focdmex  13882  hashf1rn  13884  hashge2el2dif  14011  pfxccatin12  14263  cshwidxmod  14333  cshweqdif2  14349  pfxco  14368  sinbnd  15704  cosbnd  15705  lcmfun  16165  divgcdcoprmex  16186  cncongr1  16187  vfermltlALT  16318  setsstruct2  16703  funcsetcestrclem8  17623  fullsetcestrc  17627  smndex1iidm  18282  cyccom  18564  mat1dim0  21324  mat1dimid  21325  mat1dimscm  21326  mat1dimmul  21327  dmatmul  21348  scmatcrng  21372  1marepvsma1  21434  cramerimplem1  21534  cramerimplem2  21535  cpmatacl  21567  cpmatmcllem  21569  decpmatmul  21623  pmatcollpwscmatlem1  21640  chpmat1dlem  21686  chfacfscmul0  21709  chfacfpmmul0  21713  lpbl  23355  metustsym  23407  sincosq2sgn  25343  sincosq4sgn  25345  ercgrg  26562  subupgr  27329  nbgr2vtx1edg  27392  nbuhgr2vtx1edgb  27394  cplgr3v  27477  pthdivtx  27770  usgr2wlkspthlem1  27798  usgr2wlkspthlem2  27799  wwlknbp  27880  clwlkclwwlklem2a  28035  eleclclwwlknlem2  28098  clwwlknonwwlknonb  28143  clwlknon2num  28405  numclwlk1lem1  28406  numclwlk1lem2  28407  numclwwlk7  28428  frgrreg  28431  shorth  29330  trleile  30922  oddpwdc  31987  bnj1098  32430  bnj999  32605  bnj1118  32631  segcon2  34093  pibt2  35274  lsateln0  36695  cvrcmp2  36984  dalemswapyz  37356  lhprelat3N  37740  cdleme28b  38071  qirropth  40374  nzin  41550  sigaraf  43984  sigarmf  43985  sigaras  43986  sigarms  43987  sigariz  43994  f1cof1b  44184  afvelrn  44275  elfzelfzlble  44429  prproropf1olem4  44574  prprelprb  44585  fmtnoprmfac2  44635  flsqrt  44661  proththd  44682  evensumeven  44775  evengpop3  44866  evengpoap3  44867  nnsum4primeseven  44868  nnsum4primesevenALTV  44869  tgoldbach  44885  mgmhmf1o  44957  rnghmf1o  45077  c0snmgmhm  45088  lmodvsmdi  45334  ply1mulgsumlem1  45343  lindslinindsimp1  45414  lindsrng01  45425  ldepspr  45430  digexp  45569  dig1  45570  rrx2pnedifcoorneorr  45679  rrxsphere  45710  setrec1lem3  46009