Theorem ancomd 463

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  simprd  497  jccil  524  2reu5  3755  relbrcnvg  6105  soxp  8115  ressuppssdif  8170  relelec  8748  undifixp  8928  funsnfsupp  9387  infmo  9490  fpwwe2lem12  10637  nqpr  11009  infregelb  12198  ssfzunsnext  13546  hashf1rn  14312  hashge2el2dif  14441  pfxccatin12  14683  cshwidxmod  14753  cshweqdif2  14769  pfxco  14789  sinbnd  16123  cosbnd  16124  lcmfun  16582  divgcdcoprmex  16603  cncongr1  16604  vfermltlALT  16735  setsstruct2  17107  funcsetcestrclem8  18114  fullsetcestrc  18118  smndex1iidm  18782  cyccom  19080  mat1dim0  21975  mat1dimid  21976  mat1dimscm  21977  mat1dimmul  21978  dmatmul  21999  scmatcrng  22023  1marepvsma1  22085  cramerimplem1  22185  cramerimplem2  22186  cpmatacl  22218  cpmatmcllem  22220  decpmatmul  22274  pmatcollpwscmatlem1  22291  chpmat1dlem  22337  chfacfscmul0  22360  chfacfpmmul0  22364  lpbl  24012  metustsym  24064  sincosq2sgn  26009  sincosq4sgn  26011  ercgrg  27799  subupgr  28575  nbgr2vtx1edg  28638  nbuhgr2vtx1edgb  28640  cplgr3v  28723  pthdivtx  29017  usgr2wlkspthlem1  29045  usgr2wlkspthlem2  29046  wwlknbp  29127  clwlkclwwlklem2a  29282  eleclclwwlknlem2  29345  clwwlknonwwlknonb  29390  clwlknon2num  29652  numclwlk1lem1  29653  numclwlk1lem2  29654  numclwwlk7  29675  frgrreg  29678  shorth  30579  trleile  32172  oddpwdc  33384  bnj1098  33825  bnj999  34000  bnj1118  34026  segcon2  35108  pibt2  36346  lsateln0  37913  cvrcmp2  38202  dalemswapyz  38575  lhprelat3N  38959  cdleme28b  39290  qirropth  41694  onsucf1lem  42067  omlim2  42097  tfsconcatlem  42134  tfsconcatrn  42140  tfsconcatrev  42146  nzin  43125  sigaraf  45617  sigarmf  45618  sigaras  45619  sigarms  45620  sigariz  45627  f1cof1b  45833  afvelrn  45924  elfzelfzlble  46077  prproropf1olem4  46222  prprelprb  46233  fmtnoprmfac2  46283  flsqrt  46309  proththd  46330  evensumeven  46423  evengpop3  46514  evengpoap3  46515  nnsum4primeseven  46516  nnsum4primesevenALTV  46517  tgoldbach  46533  mgmhmf1o  46605  rnghmf1o  46749  c0snmgmhm  46761  lmodvsmdi  47106  ply1mulgsumlem1  47115  lindslinindsimp1  47186  lindsrng01  47197  ldepspr  47202  digexp  47341  dig1  47342  rrx2pnedifcoorneorr  47451  rrxsphere  47482  setrec1lem3  47782