Theorem ancomd 466

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

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  simprd  500  jccil  531  2reu5  3722  relbrcnvg  6109  soxp  8126  ressuppssdif  8182  relelec  8743  undifixp  8933  funsnfsupp  9353  infmo  9458  fpwwe2lem12  10628  nqpr  11000  infregelb  12200  ssfzunsnext  13599  hashf1rn  14390  hashge2el2dif  14519  pfxccatin12  14772  cshwidxmod  14842  cshweqdif2  14858  pfxco  14877  sinbnd  16237  cosbnd  16238  lcmfun  16704  divgcdcoprmex  16725  cncongr1  16726  vfermltlALT  16863  setsstruct2  17235  funcsetcestrclem8  18219  fullsetcestrc  18223  chnccat  18683  mgmhmf1o  18759  smndex1iidm  18961  cyccom  19275  rnghmf1o  20535  c0snmgmhm  20545  quscrng  21404  mat1dim0  22611  mat1dimid  22612  mat1dimscm  22613  mat1dimmul  22614  dmatmul  22635  scmatcrng  22659  1marepvsma1  22721  cramerimplem1  22821  cramerimplem2  22822  cpmatacl  22854  cpmatmcllem  22856  decpmatmul  22910  pmatcollpwscmatlem1  22927  chpmat1dlem  22973  chfacfscmul0  22996  chfacfpmmul0  23000  lpbl  24641  metustsym  24693  sincosq2sgn  26642  sincosq4sgn  26644  ercgrg  28764  subupgr  29615  nbgr2vtx1edg  29678  nbuhgr2vtx1edgb  29680  cplgr3v  29763  pthdivtx  30054  usgr2wlkspthlem1  30084  usgr2wlkspthlem2  30085  wwlknbp  30169  clwlkclwwlklem2a  30327  eleclclwwlknlem2  30390  clwwlknonwwlknonb  30435  clwlknon2num  30697  numclwlk1lem1  30698  numclwlk1lem2  30699  numclwwlk7  30720  frgrreg  30723  shorth  31625  trleile  33269  oddpwdc  34722  bnj1098  35150  bnj999  35324  bnj1118  35350  segcon2  36575  pibt2  38041  lsateln0  39747  cvrcmp2  40036  dalemswapyz  40408  lhprelat3N  40792  cdleme28b  41123  qirropth  43615  onsucf1lem  43976  omlim2  44006  tfsconcatlem  44043  tfsconcatrn  44049  tfsconcatrev  44055  nzin  45008  sigaraf  47547  sigarmf  47548  sigaras  47549  sigarms  47550  sigariz  47557  f1cof1b  47791  afvelrn  47882  elfzelfzlble  48035  prproropf1olem4  48232  prprelprb  48243  fmtnoprmfac2  48296  flsqrt  48322  proththd  48343  evensumeven  48449  evengpop3  48540  evengpoap3  48541  nnsum4primeseven  48542  nnsum4primesevenALTV  48543  tgoldbach  48559  uhgrimisgrgric  48673  gpgedg2ov  48808  gpgedg2iv  48809  lmodvsmdi  49136  ply1mulgsumlem1  49143  lindslinindsimp1  49214  lindsrng01  49225  ldepspr  49230  digexp  49364  dig1  49365  rrx2pnedifcoorneorr  49474  rrxsphere  49505  setrec1lem3  50444