Theorem an32s 574

Description: Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.)

Hypothesis

Ref	Expression
an32s.1	|- ( ( ( ph /\ ps ) /\ ch ) -> th )

Assertion

Ref	Expression
an32s	|- ( ( ( ph /\ ch ) /\ ps ) -> th )

Proof of Theorem an32s

Step	Hyp	Ref	Expression
1		an32 568	. 2 |- ( ( ( ph /\ ch ) /\ ps ) <-> ( ( ph /\ ps ) /\ ch ) )
2		an32s.1	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	1, 2	sylbi 121	1 |- ( ( ( ph /\ ch ) /\ ps ) -> th )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  anass1rs  577  anabss1  582  biadanid  622  fssres  5565  foco  5626  fun11iun  5660  fconstfvm  5933  isocnv  6017  f1oiso  6032  f1ocnvfv3  6074  tfrcl  6635  mapxpen  7148  findcard  7192  exmidfodomrlemim  7553  genpassl  7891  genpassu  7892  axsuploc  8398  cnegexlem3  8504  recexaplem2  8982  divap0  9016  dfinfre  9288  qreccl  10051  xrlttr  10207  addmodlteq  10848  cau3lem  11895  climcn1  12090  climcn2  12091  climcaucn  12133  ntrivcvgap  12331  rplpwr  12820  dvdssq  12824  nn0seqcvgd  12835  lcmgcdlem  12871  isprm6  12942  phiprmpw  13020  pcneg  13124  prmpwdvds  13154  4sqlem19  13208  grpinveu  13892  mulgnn0subcl  13987  mulgsubcl  13988  mhmmulg  14015  ghmmulg  14108  ringrghm  14416  dvdsrcl2  14455  crngunit  14467  dvdsrpropdg  14503  lss1d  14769  quscrng  14919  mulgghm2  14992  tgcl  15214  innei  15313  cncnp  15380  cnnei  15382  elbl2ps  15542  elbl2  15543  cncfco  15741  cnlimc  15822  logdivlt  16046