Theorem ancomd 462

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  simprd  496  jccil  523  2reu5  3693  relbrcnvg  6013  soxp  7970  ressuppssdif  8001  relelec  8543  undifixp  8722  funsnfsupp  9152  infmo  9254  fpwwe2lem12  10398  nqpr  10770  infregelb  11959  ssfzunsnext  13301  focdmex  14065  hashf1rn  14067  hashge2el2dif  14194  pfxccatin12  14446  cshwidxmod  14516  cshweqdif2  14532  pfxco  14551  sinbnd  15889  cosbnd  15890  lcmfun  16350  divgcdcoprmex  16371  cncongr1  16372  vfermltlALT  16503  setsstruct2  16875  funcsetcestrclem8  17879  fullsetcestrc  17883  smndex1iidm  18540  cyccom  18822  mat1dim0  21622  mat1dimid  21623  mat1dimscm  21624  mat1dimmul  21625  dmatmul  21646  scmatcrng  21670  1marepvsma1  21732  cramerimplem1  21832  cramerimplem2  21833  cpmatacl  21865  cpmatmcllem  21867  decpmatmul  21921  pmatcollpwscmatlem1  21938  chpmat1dlem  21984  chfacfscmul0  22007  chfacfpmmul0  22011  lpbl  23659  metustsym  23711  sincosq2sgn  25656  sincosq4sgn  25658  ercgrg  26878  subupgr  27654  nbgr2vtx1edg  27717  nbuhgr2vtx1edgb  27719  cplgr3v  27802  pthdivtx  28097  usgr2wlkspthlem1  28125  usgr2wlkspthlem2  28126  wwlknbp  28207  clwlkclwwlklem2a  28362  eleclclwwlknlem2  28425  clwwlknonwwlknonb  28470  clwlknon2num  28732  numclwlk1lem1  28733  numclwlk1lem2  28734  numclwwlk7  28755  frgrreg  28758  shorth  29657  trleile  31249  oddpwdc  32321  bnj1098  32763  bnj999  32938  bnj1118  32964  segcon2  34407  pibt2  35588  lsateln0  37009  cvrcmp2  37298  dalemswapyz  37670  lhprelat3N  38054  cdleme28b  38385  qirropth  40730  nzin  41936  sigaraf  44369  sigarmf  44370  sigaras  44371  sigarms  44372  sigariz  44379  f1cof1b  44569  afvelrn  44660  elfzelfzlble  44813  prproropf1olem4  44958  prprelprb  44969  fmtnoprmfac2  45019  flsqrt  45045  proththd  45066  evensumeven  45159  evengpop3  45250  evengpoap3  45251  nnsum4primeseven  45252  nnsum4primesevenALTV  45253  tgoldbach  45269  mgmhmf1o  45341  rnghmf1o  45461  c0snmgmhm  45472  lmodvsmdi  45718  ply1mulgsumlem1  45727  lindslinindsimp1  45798  lindsrng01  45809  ldepspr  45814  digexp  45953  dig1  45954  rrx2pnedifcoorneorr  46063  rrxsphere  46094  setrec1lem3  46395