Theorem ancomd 467

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  simprd  501  jccil  532  2reu5  3719  relbrcnvg  6113  soxp  8168  ressuppssdif  8230  relelec  8793  undifixp  8990  funsnfsupp  9411  infmo  9516  setrec1lem3  9996  fpwwe2lem12  10754  nqpr  11126  infregelb  12328  ssfzunsnext  13730  hashf1rn  14523  hashge2el2dif  14652  pfxccatin12  14910  cshwidxmod  14982  cshweqdif2  14998  pfxco  15017  sinbnd  16377  cosbnd  16378  lcmfun  16849  divgcdcoprmex  16870  cncongr1  16871  vfermltlALT  17009  setsstruct2  17381  funcsetcestrclem8  18365  fullsetcestrc  18369  chnccat  18829  mgmhmf1o  18918  smndex1iidm  19126  cyccom  19447  rnghmf1o  20712  c0snmgmhm  20722  crngrhmfo  20756  quscrng  21609  mat1dim0  22818  mat1dimid  22819  mat1dimscm  22820  mat1dimmul  22821  dmatmul  22842  scmatcrng  22866  1marepvsma1  22928  cramerimplem1  23031  cramerimplem2  23032  cpmatacl  23064  cpmatmcllem  23066  decpmatmul  23120  pmatcollpwscmatlem1  23137  chpmat1dlem  23183  chfacfscmul0  23206  chfacfpmmul0  23210  lpbl  24852  metustsym  24904  sincosq2sgn  26858  sincosq4sgn  26860  ercgrg  29010  subupgr  29898  nbgr2vtx1edg  29961  nbuhgr2vtx1edgb  29963  cplgr3v  30046  pthdivtx  30342  usgr2wlkspthlem1  30373  usgr2wlkspthlem2  30374  wwlknbp  30461  clwlkclwwlklem2a  30619  eleclclwwlknlem2  30682  clwwlknonwwlknonb  30727  clwlknon2num  30999  numclwlk1lem1  31000  numclwlk1lem2  31001  numclwwlk7  31022  frgrreg  31025  shorth  31927  trleile  33602  oddpwdc  35056  bnj1098  35484  bnj999  35658  bnj1118  35684  segcon2  37048  lsateln0  40244  cvrcmp2  40533  dalemswapyz  40905  lhprelat3N  41289  cdleme28b  41620  qirropth  44108  onsucf1lem  44463  omlim2  44493  tfsconcatlem  44530  tfsconcatrn  44536  tfsconcatrev  44542  nzin  45494  sigaraf  48068  sigarmf  48069  sigaras  48070  sigarms  48071  sigariz  48078  f1cof1b  48352  afvelrn  48443  elfzelfzlble  48596  prproropf1olem4  48793  prprelprb  48804  fmtnoprmfac2  48857  flsqrt  48883  proththd  48904  evensumeven  49010  evengpop3  49101  evengpoap3  49102  nnsum4primeseven  49103  nnsum4primesevenALTV  49104  tgoldbach  49120  uhgrimisgrgric  49234  gpgedg2ov  49369  gpgedg2iv  49370  lmodvsmdi  49696  ply1mulgsumlem1  49703  lindslinindsimp1  49774  lindsrng01  49785  ldepspr  49790  digexp  49924  dig1  49925  rrx2pnedifcoorneorr  50035  rrxsphere  50065