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  3724  relbrcnvg  6112  soxp  8134  ressuppssdif  8190  relelec  8751  undifixp  8941  funsnfsupp  9362  infmo  9467  fpwwe2lem12  10645  nqpr  11017  infregelb  12217  ssfzunsnext  13616  hashf1rn  14408  hashge2el2dif  14537  pfxccatin12  14794  cshwidxmod  14866  cshweqdif2  14882  pfxco  14901  sinbnd  16261  cosbnd  16262  lcmfun  16728  divgcdcoprmex  16749  cncongr1  16750  vfermltlALT  16887  setsstruct2  17259  funcsetcestrclem8  18243  fullsetcestrc  18247  chnccat  18707  mgmhmf1o  18787  smndex1iidm  18991  cyccom  19305  rnghmf1o  20567  c0snmgmhm  20577  crngrhmfo  20611  quscrng  21460  mat1dim0  22667  mat1dimid  22668  mat1dimscm  22669  mat1dimmul  22670  dmatmul  22691  scmatcrng  22715  1marepvsma1  22777  cramerimplem1  22877  cramerimplem2  22878  cpmatacl  22910  cpmatmcllem  22912  decpmatmul  22966  pmatcollpwscmatlem1  22983  chpmat1dlem  23029  chfacfscmul0  23052  chfacfpmmul0  23056  lpbl  24697  metustsym  24749  sincosq2sgn  26701  sincosq4sgn  26703  ercgrg  28823  subupgr  29674  nbgr2vtx1edg  29737  nbuhgr2vtx1edgb  29739  cplgr3v  29822  pthdivtx  30113  usgr2wlkspthlem1  30143  usgr2wlkspthlem2  30144  wwlknbp  30228  clwlkclwwlklem2a  30386  eleclclwwlknlem2  30449  clwwlknonwwlknonb  30494  clwlknon2num  30756  numclwlk1lem1  30757  numclwlk1lem2  30758  numclwwlk7  30779  frgrreg  30782  shorth  31684  trleile  33322  oddpwdc  34776  bnj1098  35204  bnj999  35378  bnj1118  35404  segcon2  36618  pibt2  38104  lsateln0  39810  cvrcmp2  40099  dalemswapyz  40471  lhprelat3N  40855  cdleme28b  41186  qirropth  43676  onsucf1lem  44037  omlim2  44067  tfsconcatlem  44104  tfsconcatrn  44110  tfsconcatrev  44116  nzin  45069  sigaraf  47608  sigarmf  47609  sigaras  47610  sigarms  47611  sigariz  47618  f1cof1b  47855  afvelrn  47946  elfzelfzlble  48099  prproropf1olem4  48296  prprelprb  48307  fmtnoprmfac2  48360  flsqrt  48386  proththd  48407  evensumeven  48513  evengpop3  48604  evengpoap3  48605  nnsum4primeseven  48606  nnsum4primesevenALTV  48607  tgoldbach  48623  uhgrimisgrgric  48737  gpgedg2ov  48872  gpgedg2iv  48873  lmodvsmdi  49200  ply1mulgsumlem1  49207  lindslinindsimp1  49278  lindsrng01  49289  ldepspr  49294  digexp  49428  dig1  49429  rrx2pnedifcoorneorr  49538  rrxsphere  49569  setrec1lem3  50508