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  3715  relbrcnvg  6100  soxp  8143  ressuppssdif  8205  relelec  8768  undifixp  8965  funsnfsupp  9387  infmo  9492  setrec1lem3  9972  fpwwe2lem12  10730  nqpr  11102  infregelb  12304  ssfzunsnext  13706  hashf1rn  14499  hashge2el2dif  14628  pfxccatin12  14886  cshwidxmod  14958  cshweqdif2  14974  pfxco  14993  sinbnd  16353  cosbnd  16354  lcmfun  16825  divgcdcoprmex  16846  cncongr1  16847  vfermltlALT  16985  setsstruct2  17357  funcsetcestrclem8  18341  fullsetcestrc  18345  chnccat  18805  mgmhmf1o  18894  smndex1iidm  19102  cyccom  19423  rnghmf1o  20687  c0snmgmhm  20697  crngrhmfo  20731  quscrng  21584  mat1dim0  22793  mat1dimid  22794  mat1dimscm  22795  mat1dimmul  22796  dmatmul  22817  scmatcrng  22841  1marepvsma1  22903  cramerimplem1  23006  cramerimplem2  23007  cpmatacl  23039  cpmatmcllem  23041  decpmatmul  23095  pmatcollpwscmatlem1  23112  chpmat1dlem  23158  chfacfscmul0  23181  chfacfpmmul0  23185  lpbl  24827  metustsym  24879  sincosq2sgn  26833  sincosq4sgn  26835  ercgrg  28985  subupgr  29873  nbgr2vtx1edg  29936  nbuhgr2vtx1edgb  29938  cplgr3v  30021  pthdivtx  30317  usgr2wlkspthlem1  30348  usgr2wlkspthlem2  30349  wwlknbp  30436  clwlkclwwlklem2a  30594  eleclclwwlknlem2  30657  clwwlknonwwlknonb  30702  clwlknon2num  30974  numclwlk1lem1  30975  numclwlk1lem2  30976  numclwwlk7  30997  frgrreg  31000  shorth  31902  trleile  33578  oddpwdc  35032  bnj1098  35460  bnj999  35634  bnj1118  35660  segcon2  36962  lsateln0  40145  cvrcmp2  40434  dalemswapyz  40806  lhprelat3N  41190  cdleme28b  41521  qirropth  44008  onsucf1lem  44364  omlim2  44394  tfsconcatlem  44431  tfsconcatrn  44437  tfsconcatrev  44443  nzin  45395  sigaraf  47956  sigarmf  47957  sigaras  47958  sigarms  47959  sigariz  47966  f1cof1b  48240  afvelrn  48331  elfzelfzlble  48484  prproropf1olem4  48681  prprelprb  48692  fmtnoprmfac2  48745  flsqrt  48771  proththd  48792  evensumeven  48898  evengpop3  48989  evengpoap3  48990  nnsum4primeseven  48991  nnsum4primesevenALTV  48992  tgoldbach  49008  uhgrimisgrgric  49122  gpgedg2ov  49257  gpgedg2iv  49258  lmodvsmdi  49584  ply1mulgsumlem1  49591  lindslinindsimp1  49662  lindsrng01  49673  ldepspr  49678  digexp  49812  dig1  49813  rrx2pnedifcoorneorr  49923  rrxsphere  49953