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  3719  relbrcnvg  6105  soxp  8131  ressuppssdif  8187  relelec  8748  undifixp  8945  funsnfsupp  9366  infmo  9471  fpwwe2lem12  10655  nqpr  11027  infregelb  12227  ssfzunsnext  13628  hashf1rn  14420  hashge2el2dif  14549  pfxccatin12  14806  cshwidxmod  14878  cshweqdif2  14894  pfxco  14913  sinbnd  16274  cosbnd  16275  lcmfun  16741  divgcdcoprmex  16762  cncongr1  16763  vfermltlALT  16900  setsstruct2  17272  funcsetcestrclem8  18256  fullsetcestrc  18260  chnccat  18720  mgmhmf1o  18808  smndex1iidm  19016  cyccom  19337  rnghmf1o  20599  c0snmgmhm  20609  crngrhmfo  20643  quscrng  21492  mat1dim0  22701  mat1dimid  22702  mat1dimscm  22703  mat1dimmul  22704  dmatmul  22725  scmatcrng  22749  1marepvsma1  22811  cramerimplem1  22914  cramerimplem2  22915  cpmatacl  22947  cpmatmcllem  22949  decpmatmul  23003  pmatcollpwscmatlem1  23020  chpmat1dlem  23066  chfacfscmul0  23089  chfacfpmmul0  23093  lpbl  24735  metustsym  24787  sincosq2sgn  26744  sincosq4sgn  26746  ercgrg  28867  subupgr  29755  nbgr2vtx1edg  29818  nbuhgr2vtx1edgb  29820  cplgr3v  29903  pthdivtx  30199  usgr2wlkspthlem1  30230  usgr2wlkspthlem2  30231  wwlknbp  30318  clwlkclwwlklem2a  30476  eleclclwwlknlem2  30539  clwwlknonwwlknonb  30584  clwlknon2num  30856  numclwlk1lem1  30857  numclwlk1lem2  30858  numclwwlk7  30879  frgrreg  30882  shorth  31784  trleile  33419  oddpwdc  34873  bnj1098  35301  bnj999  35475  bnj1118  35501  segcon2  36693  pibt2  38179  lsateln0  39876  cvrcmp2  40165  dalemswapyz  40537  lhprelat3N  40921  cdleme28b  41252  qirropth  43757  onsucf1lem  44118  omlim2  44148  tfsconcatlem  44185  tfsconcatrn  44191  tfsconcatrev  44197  nzin  45150  sigaraf  47689  sigarmf  47690  sigaras  47691  sigarms  47692  sigariz  47699  f1cof1b  47973  afvelrn  48064  elfzelfzlble  48217  prproropf1olem4  48414  prprelprb  48425  fmtnoprmfac2  48478  flsqrt  48504  proththd  48525  evensumeven  48631  evengpop3  48722  evengpoap3  48723  nnsum4primeseven  48724  nnsum4primesevenALTV  48725  tgoldbach  48741  uhgrimisgrgric  48855  gpgedg2ov  48990  gpgedg2iv  48991  lmodvsmdi  49317  ply1mulgsumlem1  49324  lindslinindsimp1  49395  lindsrng01  49406  ldepspr  49411  digexp  49545  dig1  49546  rrx2pnedifcoorneorr  49655  rrxsphere  49686  setrec1lem3  50623