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  3716  relbrcnvg  6099  soxp  8130  ressuppssdif  8186  relelec  8749  undifixp  8946  funsnfsupp  9368  infmo  9473  setrec1lem3  9950  fpwwe2lem12  10708  nqpr  11080  infregelb  12282  ssfzunsnext  13683  hashf1rn  14476  hashge2el2dif  14605  pfxccatin12  14862  cshwidxmod  14934  cshweqdif2  14950  pfxco  14969  sinbnd  16328  cosbnd  16329  lcmfun  16800  divgcdcoprmex  16821  cncongr1  16822  vfermltlALT  16960  setsstruct2  17332  funcsetcestrclem8  18316  fullsetcestrc  18320  chnccat  18780  mgmhmf1o  18869  smndex1iidm  19077  cyccom  19398  rnghmf1o  20662  c0snmgmhm  20672  crngrhmfo  20706  quscrng  21559  mat1dim0  22768  mat1dimid  22769  mat1dimscm  22770  mat1dimmul  22771  dmatmul  22792  scmatcrng  22816  1marepvsma1  22878  cramerimplem1  22981  cramerimplem2  22982  cpmatacl  23014  cpmatmcllem  23016  decpmatmul  23070  pmatcollpwscmatlem1  23087  chpmat1dlem  23133  chfacfscmul0  23156  chfacfpmmul0  23160  lpbl  24802  metustsym  24854  sincosq2sgn  26810  sincosq4sgn  26812  ercgrg  28962  subupgr  29850  nbgr2vtx1edg  29913  nbuhgr2vtx1edgb  29915  cplgr3v  29998  pthdivtx  30294  usgr2wlkspthlem1  30325  usgr2wlkspthlem2  30326  wwlknbp  30413  clwlkclwwlklem2a  30571  eleclclwwlknlem2  30634  clwwlknonwwlknonb  30679  clwlknon2num  30951  numclwlk1lem1  30952  numclwlk1lem2  30953  numclwwlk7  30974  frgrreg  30977  shorth  31879  trleile  33514  oddpwdc  34969  bnj1098  35397  bnj999  35571  bnj1118  35597  segcon2  36840  pibt2  38308  lsateln0  40020  cvrcmp2  40309  dalemswapyz  40681  lhprelat3N  41065  cdleme28b  41396  qirropth  43868  onsucf1lem  44229  omlim2  44259  tfsconcatlem  44296  tfsconcatrn  44302  tfsconcatrev  44308  nzin  45261  sigaraf  47807  sigarmf  47808  sigaras  47809  sigarms  47810  sigariz  47817  f1cof1b  48091  afvelrn  48182  elfzelfzlble  48335  prproropf1olem4  48532  prprelprb  48543  fmtnoprmfac2  48596  flsqrt  48622  proththd  48643  evensumeven  48749  evengpop3  48840  evengpoap3  48841  nnsum4primeseven  48842  nnsum4primesevenALTV  48843  tgoldbach  48859  uhgrimisgrgric  48973  gpgedg2ov  49108  gpgedg2iv  49109  lmodvsmdi  49435  ply1mulgsumlem1  49442  lindslinindsimp1  49513  lindsrng01  49524  ldepspr  49529  digexp  49663  dig1  49664  rrx2pnedifcoorneorr  49773  rrxsphere  49804