Theorem an32s 570

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 564	. 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 )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  anass1rs  573  anabss1  578  biadanid  618  fssres  5520  foco  5579  fun11iun  5613  fconstfvm  5880  isocnv  5962  f1oiso  5977  f1ocnvfv3  6017  tfrcl  6573  mapxpen  7077  findcard  7120  exmidfodomrlemim  7472  genpassl  7804  genpassu  7805  axsuploc  8311  cnegexlem3  8415  recexaplem2  8891  divap0  8923  dfinfre  9195  qreccl  9937  xrlttr  10091  addmodlteq  10723  cau3lem  11754  climcn1  11948  climcn2  11949  climcaucn  11991  ntrivcvgap  12189  rplpwr  12678  dvdssq  12682  nn0seqcvgd  12693  lcmgcdlem  12729  isprm6  12799  phiprmpw  12874  pcneg  12978  prmpwdvds  13008  4sqlem19  13062  grpinveu  13701  mulgnn0subcl  13802  mulgsubcl  13803  mhmmulg  13830  ghmmulg  13923  ringrghm  14156  dvdsrcl2  14194  crngunit  14206  dvdsrpropdg  14242  lss1d  14479  quscrng  14629  mulgghm2  14704  tgcl  14875  innei  14974  cncnp  15041  cnnei  15043  elbl2ps  15203  elbl2  15204  cncfco  15402  cnlimc  15483