Theorem ancomd 461

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  simprd  495  jccil  522  2reu5  3717  relbrcnvg  6065  soxp  8073  ressuppssdif  8129  relelec  8685  undifixp  8876  funsnfsupp  9299  infmo  9404  fpwwe2lem12  10557  nqpr  10929  infregelb  12130  ssfzunsnext  13489  hashf1rn  14279  hashge2el2dif  14407  pfxccatin12  14660  cshwidxmod  14730  cshweqdif2  14746  pfxco  14765  sinbnd  16109  cosbnd  16110  lcmfun  16576  divgcdcoprmex  16597  cncongr1  16598  vfermltlALT  16734  setsstruct2  17105  funcsetcestrclem8  18089  fullsetcestrc  18093  chnccat  18553  mgmhmf1o  18629  smndex1iidm  18830  cyccom  19136  rnghmf1o  20392  c0snmgmhm  20402  quscrng  21242  mat1dim0  22421  mat1dimid  22422  mat1dimscm  22423  mat1dimmul  22424  dmatmul  22445  scmatcrng  22469  1marepvsma1  22531  cramerimplem1  22631  cramerimplem2  22632  cpmatacl  22664  cpmatmcllem  22666  decpmatmul  22720  pmatcollpwscmatlem1  22737  chpmat1dlem  22783  chfacfscmul0  22806  chfacfpmmul0  22810  lpbl  24451  metustsym  24503  sincosq2sgn  26468  sincosq4sgn  26470  ercgrg  28572  subupgr  29343  nbgr2vtx1edg  29406  nbuhgr2vtx1edgb  29408  cplgr3v  29491  pthdivtx  29783  usgr2wlkspthlem1  29813  usgr2wlkspthlem2  29814  wwlknbp  29898  clwlkclwwlklem2a  30056  eleclclwwlknlem2  30119  clwwlknonwwlknonb  30164  clwlknon2num  30426  numclwlk1lem1  30427  numclwlk1lem2  30428  numclwwlk7  30449  frgrreg  30452  shorth  31353  trleile  33034  oddpwdc  34492  bnj1098  34920  bnj999  35095  bnj1118  35121  segcon2  36280  pibt2  37593  lsateln0  39292  cvrcmp2  39581  dalemswapyz  39953  lhprelat3N  40337  cdleme28b  40668  qirropth  43186  onsucf1lem  43547  omlim2  43577  tfsconcatlem  43614  tfsconcatrn  43620  tfsconcatrev  43626  nzin  44595  sigaraf  47133  sigarmf  47134  sigaras  47135  sigarms  47136  sigariz  47143  f1cof1b  47359  afvelrn  47450  elfzelfzlble  47603  prproropf1olem4  47788  prprelprb  47799  fmtnoprmfac2  47849  flsqrt  47875  proththd  47896  evensumeven  47989  evengpop3  48080  evengpoap3  48081  nnsum4primeseven  48082  nnsum4primesevenALTV  48083  tgoldbach  48099  uhgrimisgrgric  48213  gpgedg2ov  48348  gpgedg2iv  48349  lmodvsmdi  48661  ply1mulgsumlem1  48668  lindslinindsimp1  48739  lindsrng01  48750  ldepspr  48755  digexp  48889  dig1  48890  rrx2pnedifcoorneorr  48999  rrxsphere  49030  setrec1lem3  49970